Step | Hyp | Ref
| Expression |
1 | | eeanv 1913 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif)
Nc ![E.](exists.gif)
Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
3 | | 0ex 4110 |
. . . . . . . . 9
![_V](rmcv.gif) |
4 | 3 | complex 4104 |
. . . . . . . 8
∼ ![_V](rmcv.gif) |
5 | 2, 4 | xpsnen 6049 |
. . . . . . 7
![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![x](_x.gif) |
6 | | snex 4111 |
. . . . . . . . 9
∼ ![(/)](varnothing.gif) ![_V](rmcv.gif) |
7 | 2, 6 | xpex 5115 |
. . . . . . . 8
![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
8 | 7 | eqnc 6127 |
. . . . . . 7
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![x](_x.gif) ![)](rp.gif) |
9 | 5, 8 | mpbir 200 |
. . . . . 6
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![x](_x.gif) |
10 | 9 | eqeq2i 2363 |
. . . . 5
![(](lp.gif) Nc ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![x](_x.gif) ![)](rp.gif) |
11 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
12 | 11, 3 | xpsnen 6049 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![y](_y.gif) |
13 | | snex 4111 |
. . . . . . . . 9
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
14 | 11, 13 | xpex 5115 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
15 | 14 | eqnc 6127 |
. . . . . . 7
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![y](_y.gif) ![)](rp.gif) |
16 | 12, 15 | mpbir 200 |
. . . . . 6
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![y](_y.gif) |
17 | 16 | eqeq2i 2363 |
. . . . 5
![(](lp.gif) Nc ![(](lp.gif)
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![y](_y.gif) ![)](rp.gif) |
18 | 10, 17 | anbi12i 678 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | 2exbii 1583 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc
Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | elncs 6119 |
. . . 4
![(](lp.gif) NC ![E.](exists.gif) Nc ![x](_x.gif) ![)](rp.gif) |
21 | | elncs 6119 |
. . . 4
![(](lp.gif) NC ![E.](exists.gif) Nc ![y](_y.gif) ![)](rp.gif) |
22 | 20, 21 | anbi12i 678 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
Nc ![E.](exists.gif)
Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 1, 19, 22 | 3bitr4ri 269 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 7 | ncelncsi 6121 |
. . . . . . 7
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
NC |
25 | 14 | ncelncsi 6121 |
. . . . . . 7
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
NC |
26 | | ncaddccl 6144 |
. . . . . . 7
![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) NC Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
NC Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC ![)](rp.gif) |
27 | 24, 25, 26 | mp2an 653 |
. . . . . 6
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC |
28 | | tccl 6160 |
. . . . . 6
![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC ![)](rp.gif) |
29 | 27, 28 | ax-mp 5 |
. . . . 5
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
NC |
30 | | tccl 6160 |
. . . . . . 7
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
NC Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
NC ![)](rp.gif) |
31 | 24, 30 | ax-mp 5 |
. . . . . 6
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) NC |
32 | | tccl 6160 |
. . . . . . 7
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
NC Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
NC ![)](rp.gif) |
33 | 25, 32 | ax-mp 5 |
. . . . . 6
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) NC |
34 | | ncaddccl 6144 |
. . . . . 6
![(](lp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
NC Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
NC Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC ![)](rp.gif) |
35 | 31, 33, 34 | mp2an 653 |
. . . . 5
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC |
36 | 7 | ncid 6123 |
. . . . . . 7
![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
37 | 14 | ncid 6123 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
38 | | necompl 3544 |
. . . . . . . 8
∼ ![(/)](varnothing.gif) |
39 | 4, 38 | xpnedisj 5513 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(/)](varnothing.gif) |
40 | | eladdci 4399 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 36, 37, 39, 40 | mp3an 1277 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | pw1eltc 6162 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
NC ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) 1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 27, 41, 42 | mp2an 653 |
. . . . 5
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | pw1un 4163 |
. . . . . 6
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
45 | | pw1eltc 6162 |
. . . . . . . 8
![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) NC ![(](lp.gif) ∼
![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 24, 36, 45 | mp2an 653 |
. . . . . . 7
1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
47 | | pw1eltc 6162 |
. . . . . . . 8
![(](lp.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) NC ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) 1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 25, 37, 47 | mp2an 653 |
. . . . . . 7
1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Tc
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
49 | | pw1eq 4143 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
1 ![(/)](varnothing.gif) ![)](rp.gif) |
50 | 39, 49 | ax-mp 5 |
. . . . . . . 8
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) 1 ![(/)](varnothing.gif) |
51 | | pw1in 4164 |
. . . . . . . 8
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | pw10 4161 |
. . . . . . . 8
1 ![(/)](varnothing.gif) |
53 | 50, 51, 52 | 3eqtr3i 2381 |
. . . . . . 7
![(](lp.gif) 1 ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) 1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(/)](varnothing.gif) |
54 | | eladdci 4399 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) 1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![(](lp.gif) 1 ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 46, 48, 53, 54 | mp3an 1277 |
. . . . . 6
![(](lp.gif) 1 ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) 1 ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 44, 55 | eqeltri 2423 |
. . . . 5
1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
57 | | nceleq 6149 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) NC ![(](lp.gif) 1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) 1 ![(](lp.gif) ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 29, 35, 43, 56, 57 | mp4an 654 |
. . . 4
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
59 | | addceq12 4385 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![B](_cb.gif)
Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | | tceq 6158 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![B](_cb.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc ![(](lp.gif)
![B](_cb.gif)
Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 59, 60 | syl 15 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc ![(](lp.gif) ![B](_cb.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | | tceq 6158 |
. . . . . 6
![(](lp.gif) Nc ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 62 | adantr 451 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
64 | | tceq 6158 |
. . . . . 6
![(](lp.gif) Nc ![(](lp.gif)
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | adantl 452 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 63, 65 | addceq12d 4391 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc Tc ![B](_cb.gif) Tc Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Tc Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 58, 61, 66 | 3eqtr4a 2411 |
. . 3
![(](lp.gif) ![(](lp.gif) Nc ![(](lp.gif) ∼ ![(/)](varnothing.gif) ![}](rbrace.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc ![(](lp.gif) ![B](_cb.gif) Tc Tc ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 67 | exlimivv 1635 |
. 2
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc ![(](lp.gif)
∼ ![(/)](varnothing.gif) ![}](rbrace.gif) Nc ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Tc ![(](lp.gif)
![B](_cb.gif)
Tc Tc ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 23, 68 | sylbi 187 |
1
![(](lp.gif) ![(](lp.gif) NC NC Tc ![(](lp.gif)
![B](_cb.gif)
Tc Tc ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |