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

Theorem 2moOLD 2364
 Description: Obsolete proof of 2mo 2363 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
2moOLD
Distinct variable groups:   ,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem 2moOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 equequ2 1742 . . . . . . 7
2 equequ2 1742 . . . . . . 7
31, 2bi2anan9 863 . . . . . 6
43imbi2d 316 . . . . 5
542albidv 1686 . . . 4
65cbvex2v 1984 . . 3
7 nfv 1678 . . . . . . . . 9
8 nfv 1678 . . . . . . . . 9
9 nfs1v 2149 . . . . . . . . . 10
10 nfv 1678 . . . . . . . . . 10
119, 10nfim 1857 . . . . . . . . 9
12 nfs1v 2149 . . . . . . . . . . 11
1312nfsb 2153 . . . . . . . . . 10
14 nfv 1678 . . . . . . . . . 10
1513, 14nfim 1857 . . . . . . . . 9
16 sbequ12 1941 . . . . . . . . . . 11
17 sbequ12 1941 . . . . . . . . . . 11
1816, 17sylan9bbr 695 . . . . . . . . . 10
19 equequ1 1741 . . . . . . . . . . 11
20 equequ1 1741 . . . . . . . . . . 11
2119, 20bi2anan9 863 . . . . . . . . . 10
2218, 21imbi12d 320 . . . . . . . . 9
237, 8, 11, 15, 22cbval2 1980 . . . . . . . 8
2423biimpi 194 . . . . . . 7
2524ancli 548 . . . . . 6
26 alcom 1788 . . . . . . . . 9
278, 15aaan 1907 . . . . . . . . . 10
2827albii 1615 . . . . . . . . 9
2926, 28bitri 249 . . . . . . . 8
3029albii 1615 . . . . . . 7
31 nfv 1678 . . . . . . . 8
3211nfal 1877 . . . . . . . 8
3331, 32aaan 1907 . . . . . . 7
3430, 33bitri 249 . . . . . 6
3525, 34sylibr 212 . . . . 5
36 prth 568 . . . . . . . 8
37 equtr2 1745 . . . . . . . . . 10
38 equtr2 1745 . . . . . . . . . 10
3937, 38anim12i 563 . . . . . . . . 9
4039an4s 817 . . . . . . . 8
4136, 40syl6 33 . . . . . . 7
42412alimi 1610 . . . . . 6
43422alimi 1610 . . . . 5
4435, 43syl 16 . . . 4
4544exlimivv 1694 . . 3
466, 45sylbir 213 . 2
47 alrot4 1790 . . . . 5
48 pm3.21 446 . . . . . . . . . . . 12
4948imim1d 75 . . . . . . . . . . 11
5013, 49alimd 1815 . . . . . . . . . 10
519, 50alimd 1815 . . . . . . . . 9
5251com12 31 . . . . . . . 8
5352alimi 1609 . . . . . . 7
54 exim 1628 . . . . . . 7
5553, 54syl 16 . . . . . 6
5655alimi 1609 . . . . 5
5747, 56sylbi 195 . . . 4
58 exim 1628 . . . 4
5957, 58syl 16 . . 3
60 alnex 1593 . . . . . 6
6160albii 1615 . . . . 5
62 alnex 1593 . . . . 5
6361, 62bitri 249 . . . 4
64 nfv 1678 . . . . . . 7
65 nfv 1678 . . . . . . 7
669nfn 1840 . . . . . . 7
6713nfn 1840 . . . . . . 7
6818notbid 294 . . . . . . 7
6964, 65, 66, 67, 68cbval2 1980 . . . . . 6
70 pm2.21 108 . . . . . . 7
71702alimi 1610 . . . . . 6
7269, 71sylbir 213 . . . . 5
73 19.8a 1798 . . . . . 6
747319.23bi 1810 . . . . 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 1362  wex 1591  wsb 1705 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator