Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2moOLDOLD Structured version   Unicode version

Theorem 2moOLDOLD 2384
 Description: Obsolete proof of 2mo 2382 as of 19-Jan-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
2moOLDOLD
Distinct variable groups:   ,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem 2moOLDOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 equequ2 1748 . . . . . . 7
2 equequ2 1748 . . . . . . 7
31, 2bi2anan9 871 . . . . . 6
43imbi2d 316 . . . . 5
542albidv 1691 . . . 4
65cbvex2v 2004 . . 3
7 nfv 1683 . . . . . . . . 9
8 nfv 1683 . . . . . . . . 9
9 nfs1v 2164 . . . . . . . . . 10
10 nfv 1683 . . . . . . . . . 10
119, 10nfim 1867 . . . . . . . . 9
12 nfs1v 2164 . . . . . . . . . . 11
1312nfsb 2168 . . . . . . . . . 10
14 nfv 1683 . . . . . . . . . 10
1513, 14nfim 1867 . . . . . . . . 9
16 sbequ12 1961 . . . . . . . . . . 11
17 sbequ12 1961 . . . . . . . . . . 11
1816, 17sylan9bbr 700 . . . . . . . . . 10
19 equequ1 1747 . . . . . . . . . . 11
20 equequ1 1747 . . . . . . . . . . 11
2119, 20bi2anan9 871 . . . . . . . . . 10
2218, 21imbi12d 320 . . . . . . . . 9
237, 8, 11, 15, 22cbval2 2000 . . . . . . . 8
2423biimpi 194 . . . . . . 7
2524ancli 551 . . . . . 6
26 alcom 1794 . . . . . . . . 9
278, 15aaan 1924 . . . . . . . . . 10
2827albii 1620 . . . . . . . . 9
2926, 28bitri 249 . . . . . . . 8
3029albii 1620 . . . . . . 7
31 nfv 1683 . . . . . . . 8
3211nfal 1894 . . . . . . . 8
3331, 32aaan 1924 . . . . . . 7
3430, 33bitri 249 . . . . . 6
3525, 34sylibr 212 . . . . 5
36 prth 571 . . . . . . . 8
37 equtr2 1751 . . . . . . . . . 10
38 equtr2 1751 . . . . . . . . . 10
3937, 38anim12i 566 . . . . . . . . 9
4039an4s 824 . . . . . . . 8
4136, 40syl6 33 . . . . . . 7
42412alimi 1615 . . . . . 6
43422alimi 1615 . . . . 5
4435, 43syl 16 . . . 4
4544exlimivv 1699 . . 3
466, 45sylbir 213 . 2
47 alrot4 1796 . . . . 5
48 pm3.21 448 . . . . . . . . . . . 12
4948imim1d 75 . . . . . . . . . . 11
5013, 49alimd 1824 . . . . . . . . . 10
519, 50alimd 1824 . . . . . . . . 9
5251com12 31 . . . . . . . 8
5352alimi 1614 . . . . . . 7
54 exim 1633 . . . . . . 7
5553, 54syl 16 . . . . . 6
5655alimi 1614 . . . . 5
5747, 56sylbi 195 . . . 4
58 exim 1633 . . . 4
5957, 58syl 16 . . 3
60 alnex 1598 . . . . . 6
6160albii 1620 . . . . 5
62 alnex 1598 . . . . 5
6361, 62bitri 249 . . . 4
64 nfv 1683 . . . . . . 7
65 nfv 1683 . . . . . . 7
669nfn 1849 . . . . . . 7
6713nfn 1849 . . . . . . 7
6818notbid 294 . . . . . . 7
6964, 65, 66, 67, 68cbval2 2000 . . . . . 6
70 pm2.21 108 . . . . . . 7
71702alimi 1615 . . . . . 6
7269, 71sylbir 213 . . . . 5
73 19.8a 1806 . . . . . 6
747319.23bi 1819 . . . . 5
7572, 74syl 16 . . . 4
7663, 75sylbir 213 . . 3
7759, 76pm2.61d1 159 . 2
7846, 77impbii 188 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369  wal 1377  wex 1596  wsb 1711 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator