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

Theorem 2eu6OLD 2362
 Description: Obsolete proof of 2eu6 2361 as of 21-Sep-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
2eu6OLD
Distinct variable groups:   ,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem 2eu6OLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2eu4 2358 . 2
2 nfv 1754 . . . . . 6
3 nfv 1754 . . . . . 6
4 nfs1v 2233 . . . . . 6
5 nfs1v 2233 . . . . . . 7
65nfsb 2236 . . . . . 6
7 sbequ12 2049 . . . . . . 7
8 sbequ12 2049 . . . . . . 7
97, 8sylan9bbr 705 . . . . . 6
102, 3, 4, 6, 9cbvex2 2084 . . . . 5
11 equequ2 1851 . . . . . . . . . 10
12 equequ2 1851 . . . . . . . . . 10
1311, 12bi2anan9 881 . . . . . . . . 9
1413imbi2d 317 . . . . . . . 8
15142albidv 1762 . . . . . . 7
1615cbvex2v 2086 . . . . . 6
17 nfv 1754 . . . . . . . . 9
18 nfv 1754 . . . . . . . . 9
19 nfv 1754 . . . . . . . . . 10
204, 19nfim 1978 . . . . . . . . 9
21 nfv 1754 . . . . . . . . . 10
226, 21nfim 1978 . . . . . . . . 9
23 equequ1 1850 . . . . . . . . . . 11
24 equequ1 1850 . . . . . . . . . . 11
2523, 24bi2anan9 881 . . . . . . . . . 10
269, 25imbi12d 321 . . . . . . . . 9
2717, 18, 20, 22, 26cbval2 2083 . . . . . . . 8
28272exbii 1715 . . . . . . 7
29 2mo 2351 . . . . . . 7
3028, 29bitri 252 . . . . . 6
3116, 30bitri 252 . . . . 5
32 19.29r2 1732 . . . . 5
3310, 31, 32syl2anb 481 . . . 4
34 2albiim 1747 . . . . . . 7
35 ancom 451 . . . . . . 7
3634, 35bitri 252 . . . . . 6
37362exbii 1715 . . . . 5
38 nfv 1754 . . . . . . . . . . . 12
39 nfv 1754 . . . . . . . . . . . 12
404nfsb 2236 . . . . . . . . . . . . . . 15
4140nfsb 2236 . . . . . . . . . . . . . 14
424, 41nfan 1986 . . . . . . . . . . . . 13
4342, 19nfim 1978 . . . . . . . . . . . 12
446nfsb 2236 . . . . . . . . . . . . . . 15
4544nfsb 2236 . . . . . . . . . . . . . 14
466, 45nfan 1986 . . . . . . . . . . . . 13
4746, 21nfim 1978 . . . . . . . . . . . 12
48 sbequ12 2049 . . . . . . . . . . . . . . . 16
49 sbequ12 2049 . . . . . . . . . . . . . . . 16
5048, 49sylan9bbr 705 . . . . . . . . . . . . . . 15
513sbco2 2210 . . . . . . . . . . . . . . . . 17
5251sbbii 1796 . . . . . . . . . . . . . . . 16
53 nfv 1754 . . . . . . . . . . . . . . . . . 18
5453sbco2 2210 . . . . . . . . . . . . . . . . 17
55 sbcom2 2241 . . . . . . . . . . . . . . . . . 18
5655sbbii 1796 . . . . . . . . . . . . . . . . 17
5754, 56bitr3i 254 . . . . . . . . . . . . . . . 16
5852, 57bitr3i 254 . . . . . . . . . . . . . . 15
5950, 58syl6bb 264 . . . . . . . . . . . . . 14
6059anbi2d 708 . . . . . . . . . . . . 13
61 equequ2 1851 . . . . . . . . . . . . . 14
62 equequ2 1851 . . . . . . . . . . . . . 14
6361, 62bi2anan9 881 . . . . . . . . . . . . 13
6460, 63imbi12d 321 . . . . . . . . . . . 12
6538, 39, 43, 47, 64cbval2 2083 . . . . . . . . . . 11
66 equcom 1846 . . . . . . . . . . . . . . 15
67 equcom 1846 . . . . . . . . . . . . . . 15
6866, 67anbi12i 701 . . . . . . . . . . . . . 14
6968imbi2i 313 . . . . . . . . . . . . 13
70 impexp 447 . . . . . . . . . . . . 13
7169, 70bitri 252 . . . . . . . . . . . 12
72712albii 1688 . . . . . . . . . . 11
7365, 72bitr3i 254 . . . . . . . . . 10
744, 619.21-2 1963 . . . . . . . . . 10
7573, 74bitri 252 . . . . . . . . 9
7675anbi2i 698 . . . . . . . 8
77 abai 802 . . . . . . . 8
7876, 77bitr4i 255 . . . . . . 7
79 2sb6 2240 . . . . . . . 8
8079anbi1i 699 . . . . . . 7
8178, 80bitri 252 . . . . . 6
82812exbii 1715 . . . . 5
8337, 82bitr4i 255 . . . 4
8433, 83sylibr 215 . . 3
85 biimpr 201 . . . . . . 7
86852alimi 1681 . . . . . 6
87862eximi 1704 . . . . 5
88 2exsb 2265 . . . . 5
8987, 88sylibr 215 . . . 4
90 biimp 196 . . . . . 6
91902alimi 1681 . . . . 5
92912eximi 1704 . . . 4
9389, 92jca 534 . . 3
9484, 93impbii 190 . 2
951, 94bitri 252 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370  wal 1435  wex 1659  wsb 1789  weu 2266 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator