A list of proof subsequences which are often repeated in set.mm proofs

lemmata_suggestions

(["fvex","eqeltri"],791)
(["rspcev","syl2anc"],515)
(["syl2anc","mpbird"],363)
(["syl","mpbird"],348)
(["hllat","syl"],341)
(["anbi12d","rspcev","syl12anc"],330)
(["syl2anc","mpbid"],315)
(["ffn","syl"],306)
(["frn","syl"],304)
(["fdm","syl"],286)
(["fvex","eqeltri","a1i"],282)
(["syl","mpbid"],274)
(["eqeq2d","rspcev","syl2anc"],268)
(["syl","adantr"],268)
(["ne0i","syl"],247)
(["oveq2d","eqtrd"],244)
(["ralbidv","rspcev","syl2anc"],242)
(["eqeltri","a1i"],234)
(["syl3anc","mpbid"],234)
(["anbi12d","rspcev"],230)
(["syl","eqtrd"],229)
(["eqid","fmptd"],223)
(["oveq1","fveq2d"],223)
(["jca","ex"],217)
(["fvex","eqeltri","mptex"],172)
(["breq2","ralbidv","rspcev","syl2anc"],162)
(["breq2","ralbidv","rspcev"],140)
(["fvex","eqeltri","mptex","fvmpt"],138)
(["latjle12","syl13anc","mpbi2and"],136)
(["fdm","syl","syl5sseq"],130)
(["eqeq1d","rspcev","syl2anc"],124)
(["restid","ax-mp","eqcomi"],124)
(["fvex","eqeltri","mptex","fvmpt","syl"],120)
(["2re","2pos","pm3.2i"],120)
(["ex","reximdva","mpd"],116)
(["rspcev","syl2anc","ex"],112)
(["imbi1d","ralbidv","rspcev","syl2anc"],108)
(["ovex","fvmpt","syl"],106)
(["ex","ssrdv","eqssd"],104)
(["imbi1d","ralbidv","rspcev"],98)
(["eqeq2d","anbi12d","rspcev"],96)
(["toponunii","restid","ax-mp","eqcomi"],93)
(["eqeltri","mptex","fvmpt"],92)
(["eqeltri","mptex","fvmpt","syl"],90)
(["sseq1","anbi12d","rspcev","syl12anc"],90)
(["eqtr4d","pm2.61i","eqtri"],90)
(["0re","1re","elicc2i"],88)
(["2re","2pos","pm3.2i","a1i"],87)
(["eqeq2d","anbi12d","rspcev","syl12anc"],84)
(["eqeq12d","syl5ibr","expcom","a2d"],75)
(["fveq2","eqeq2d","rspcev","syl2anc"],69)
(["breq2","imbi1d","ralbidv","rspcev","syl2anc"],64)
(["a2d","syld","expcom","a2d","uzind4","mpcom","mpd"],60)
(["expr","a2d","syld","expcom","a2d"],60)
(["oveq2","oveq1d","fveq2d","oveq1d","oveq12d"],60)
(["imbi12d","rspcv","syl","mpid"],60)
(["oveq1","eqeq2d","rspcev","syl2anc"],60)
(["oveq2","eqeq1d","anbi12d","ralbidv"],60)
(["elrnmpt","ax-mp","biimpi","adantl"],57)
(["fveq2","eqeq1d","rspcev","syl2anc"],57)
(["fvex","eqeltri","mptex","a1i"],57)
(["jca","ex","reximdv2","mpd"],57)
(["oveq1","0p1e1","syl6eq","fveq2d"],57)
(["restid","ax-mp","eqcomi","cncfcn"],57)
(["sseq1d","anbi12d","rspcev","syl12anc"],57)
(["toponunii","restid","ax-mp","eqcomi","cncfcn"],56)
(["expr","a2d","syld","expcom","a2d","uzind4","mpcom"],54)
(["a2d","syld","expcom","a2d","uzind4","mpcom"],50)
(["oveq2","oveq1d","fveq2d","oveq1d","oveq12d","cbvmptv"],50)
(["syld","expcom","a2d","uzind4","mpcom","mpd"],50)
(["imaeq1d","xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv"],48)
(["xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv","eqeq2d"],48)
(["eqeq12d","syl5ibr","expcom","a2d","nn0ind"],48)
(["breq2","anbi2d","imbi1d","ralbidv","rspcev","syl2anc"],45)
(["expr","a2d","syld","expcom","a2d","uzind4"],45)
(["fvprc","syl5eq","fveq2d","3eqtr4a","pm2.61i"],44)
(["fvprc","syl5eq","rneqd","rn0","syl6eq"],44)
(["fzsn","syl","eqtrd","uneq2d","eqtrd"],44)
(["ovex","fvmpt","oveqan12d","adantl","3eqtr4d"],44)
(["eqeq12d","syl5ibr","expr","a2d","syld","expcom","a2d"],42)
(["imaeq1d","xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd"],40)
(["toponunii","restid","ax-mp","eqcomi","cncfcn","mp2an"],40)
(["uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv","eqeq2d"],40)
(["xpeq1d","uneq12d","oveq12d","csbeq2dv","eqtrd","mpteq2dv"],40)
(["a2d","syld","expcom","a2d","uzind4"],40)
(["breq1","imbi1d","ralbidv","rspcev","syl2anc"],40)
(["breq2","anbi2d","imbi1d","ralbidv","rspcev"],40)
(["cnfldtopon","toponunii","restid","ax-mp","eqcomi"],40)
(["expcom","a2d","uzind4","mpcom","mpd"],40)
(["fveq2","oveq1d","fveq2d","breq1d","imbi12d"],40)
(["oveq1","eleq1d","rexbidv","cbvrabv","uneq2i"],40)
(["syld","expcom","a2d","uzind4","mpcom"],40)
(["a2d","syl5","expcom","a2d","adantl","findcard2s","mpcom"],36)
(["oveq1","oveq2d","oveq2d","eqeq1d","anbi12d","rspc2ev","syl112anc"],36)
(["syl5","expcom","a2d","adantl","findcard2s","mpcom","mpi"],36)
(["oveq1d","fveq2d","oveq1d","oveq12d","cbvmptv"],36)
(["sylan2","anassrs","ralbidva","rexbidva","ralbidv"],36)
(["breq2","anbi12d","imbi1d","2ralbidv","rspcev","syl2anc"],35)
(["breq2","imbi1d","ralbidv","rspcev","syl2anc","ralrimivva"],35)
(["cbvral","a1i","bitrd","cbvrexv","a1i","bitrd"],35)
(["eqeq12d","syl5ibr","expr","a2d","syld","expcom"],35)
(["fvprc","syl5eq","rneqd","rn0","syl6eq","nsyl2"],35)
(["ltle","syl2anc","sylbid","impr","sylan2b","ralrimiva"],35)
(["reex","reex","xpex","inex2","nnex","elmap"],35)
(["syl5ibr","expr","a2d","syld","expcom","a2d"],35)
(["cbvrex","a1i","bitrd","cbvralv","a1i","bitrd","cbvrexv"],30)
(["elequ2","anbi1d","exbidv","bibi2d","albidv","imbi2d","exbidv"],30)
(["fveq2","sseq1d","anbi12d","rspcev","syl12anc","rexlimddv","ralrimivva"],30)
(["nfop","nfcxfr","nffv","nfop","nfsn","nfun","nfcxfr"],30)
(["nfres","nfop","nfcxfr","nffv","nfop","nfsn","nfun"],30)
(["releldm","ex","syl","sylbird","mpan2i","impbid","bitrd"],30)
(["syl5ibr","expr","a2d","syld","expcom","a2d","uzind4"],30)
(["oveq2d","oveq2d","eqeq1d","anbi12d","rspc2ev","syl112anc"],30)
(["ovex","fvmpt","oveqan12d","adantl","3eqtr4d","ralrimivva"],30)
(["syl5","expcom","a2d","adantl","findcard2s","mpcom"],30)
(["rexeqbidv","rexeqbidv","rexeqbidv","rspcev","syl2anc","ex","impbid"],24)
(["rexeqbidv","rexeqbidv","rspcev","syl2anc","ex","impbid","syl5bb"],24)
(["syl","eleq2d","biimpa","sylbi","a1i","rexlimi","syl"],24)
(["syl5","expcom","adantl","a2d","findcard2s","mpcom","mpi"],24)
(["syl6eq","eleq1d","syl5ibrcom","expimpd","rexlimdvva","syl5bi","ralrimiv"],24)