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

Theorem 2eu6OLD 2384
Description: Obsolete proof of 2eu6 2383 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:   , , ,   , ,

Proof of Theorem 2eu6OLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2eu4 2380 . 2
2 nfv 1707 . . . . . 6
3 nfv 1707 . . . . . 6
4 nfs1v 2181 . . . . . 6
5 nfs1v 2181 . . . . . . 7
65nfsb 2184 . . . . . 6
7 sbequ12 1992 . . . . . . 7
8 sbequ12 1992 . . . . . . 7
97, 8sylan9bbr 700 . . . . . 6
102, 3, 4, 6, 9cbvex2 2028 . . . . 5
11 equequ2 1799 . . . . . . . . . 10
12 equequ2 1799 . . . . . . . . . 10
1311, 12bi2anan9 873 . . . . . . . . 9
1413imbi2d 316 . . . . . . . 8
15142albidv 1715 . . . . . . 7
1615cbvex2v 2031 . . . . . 6
17 nfv 1707 . . . . . . . . 9
18 nfv 1707 . . . . . . . . 9
19 nfv 1707 . . . . . . . . . 10
204, 19nfim 1920 . . . . . . . . 9
21 nfv 1707 . . . . . . . . . 10
226, 21nfim 1920 . . . . . . . . 9
23 equequ1 1798 . . . . . . . . . . 11
24 equequ1 1798 . . . . . . . . . . 11
2523, 24bi2anan9 873 . . . . . . . . . 10
269, 25imbi12d 320 . . . . . . . . 9
2717, 18, 20, 22, 26cbval2 2027 . . . . . . . 8
28272exbii 1668 . . . . . . 7
29 2mo 2373 . . . . . . 7
3028, 29bitri 249 . . . . . 6
3116, 30bitri 249 . . . . 5
32 19.29r2 1685 . . . . 5
3310, 31, 32syl2anb 479 . . . 4
34 2albiim 1700 . . . . . . 7
35 ancom 450 . . . . . . 7
3634, 35bitri 249 . . . . . 6
37362exbii 1668 . . . . 5
38 nfv 1707 . . . . . . . . . . . 12
39 nfv 1707 . . . . . . . . . . . 12
404nfsb 2184 . . . . . . . . . . . . . . 15
4140nfsb 2184 . . . . . . . . . . . . . 14
424, 41nfan 1928 . . . . . . . . . . . . 13
4342, 19nfim 1920 . . . . . . . . . . . 12
446nfsb 2184 . . . . . . . . . . . . . . 15
4544nfsb 2184 . . . . . . . . . . . . . 14
466, 45nfan 1928 . . . . . . . . . . . . 13
4746, 21nfim 1920 . . . . . . . . . . . 12
48 sbequ12 1992 . . . . . . . . . . . . . . . 16
49 sbequ12 1992 . . . . . . . . . . . . . . . 16
5048, 49sylan9bbr 700 . . . . . . . . . . . . . . 15
513sbco2 2158 . . . . . . . . . . . . . . . . 17
5251sbbii 1746 . . . . . . . . . . . . . . . 16
53 nfv 1707 . . . . . . . . . . . . . . . . . 18
5453sbco2 2158 . . . . . . . . . . . . . . . . 17
55 sbcom2 2189 . . . . . . . . . . . . . . . . . 18
5655sbbii 1746 . . . . . . . . . . . . . . . . 17
5754, 56bitr3i 251 . . . . . . . . . . . . . . . 16
5852, 57bitr3i 251 . . . . . . . . . . . . . . 15
5950, 58syl6bb 261 . . . . . . . . . . . . . 14
6059anbi2d 703 . . . . . . . . . . . . 13
61 equequ2 1799 . . . . . . . . . . . . . 14
62 equequ2 1799 . . . . . . . . . . . . . 14
6361, 62bi2anan9 873 . . . . . . . . . . . . 13
6460, 63imbi12d 320 . . . . . . . . . . . 12
6538, 39, 43, 47, 64cbval2 2027 . . . . . . . . . . 11
66 equcom 1794 . . . . . . . . . . . . . . 15
67 equcom 1794 . . . . . . . . . . . . . . 15
6866, 67anbi12i 697 . . . . . . . . . . . . . 14
6968imbi2i 312 . . . . . . . . . . . . 13
70 impexp 446 . . . . . . . . . . . . 13
7169, 70bitri 249 . . . . . . . . . . . 12
72712albii 1641 . . . . . . . . . . 11
7365, 72bitr3i 251 . . . . . . . . . 10
744, 619.21-2 1906 . . . . . . . . . 10
7573, 74bitri 249 . . . . . . . . 9
7675anbi2i 694 . . . . . . . 8
77 abai 795 . . . . . . . 8
7876, 77bitr4i 252 . . . . . . 7
79 2sb6 2188 . . . . . . . 8
8079anbi1i 695 . . . . . . 7
8178, 80bitri 249 . . . . . 6
82812exbii 1668 . . . . 5
8337, 82bitr4i 252 . . . 4
8433, 83sylibr 212 . . 3
85 bi2 198 . . . . . . 7
86852alimi 1634 . . . . . 6
87862eximi 1657 . . . . 5
88 2exsb 2213 . . . . 5
8987, 88sylibr 212 . . . 4
90 bi1 186 . . . . . 6
91902alimi 1634 . . . . 5
92912eximi 1657 . . . 4
9389, 92jca 532 . . 3
9484, 93impbii 188 . 2
951, 94bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  [wsb 1739  E!weu 2282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator