Step | Hyp | Ref
| Expression |
1 | | breq2 4643 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) c c ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | breq1 4642 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 1, 2 | orbi12d 690 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
c c ![A](_ca.gif) ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | imbi2d 307 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | elun 3220 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif)
c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | eliniseg 5020 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c ![n](_n.gif) ![)](rp.gif) |
7 | | elimasn 5019 |
. . . . . . . . . . . . . 14
![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) c ![)](rp.gif) |
8 | | df-br 4640 |
. . . . . . . . . . . . . 14
![(](lp.gif) c
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) c ![)](rp.gif) |
9 | 7, 8 | bitr4i 243 |
. . . . . . . . . . . . 13
![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c ![a](_a.gif) ![)](rp.gif) |
10 | 6, 9 | orbi12i 507 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif)
c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 5, 10 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif)
c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | abbi2i 2464 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) |
13 | 12 | uneq2i 3415 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif)
Nn ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif)
Nn ![{](lbrace.gif) ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
14 | | unab 3521 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif)
Nn ![{](lbrace.gif) ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) ![{](lbrace.gif)
![(](lp.gif)
Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
15 | 13, 14 | eqtri 2373 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif)
Nn ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif)
Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
16 | | imor 401 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif)
c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | abbii 2465 |
. . . . . . . 8
![{](lbrace.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif)
Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
18 | 15, 17 | eqtr4i 2376 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif)
Nn ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif) Nn ![(](lp.gif)
c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
19 | | abexv 4324 |
. . . . . . . 8
![{](lbrace.gif) Nn ![_V](rmcv.gif) |
20 | | lecex 6115 |
. . . . . . . . . . 11
c ![_V](rmcv.gif) |
21 | 20 | cnvex 5102 |
. . . . . . . . . 10
c ![_V](rmcv.gif) |
22 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![n](_n.gif)
![_V](rmcv.gif) |
23 | 21, 22 | imaex 4747 |
. . . . . . . . 9
![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
24 | 20, 22 | imaex 4747 |
. . . . . . . . 9
c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
25 | 23, 24 | unex 4106 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![_V](rmcv.gif) |
26 | 19, 25 | unex 4106 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif)
Nn ![(](lp.gif) ![(](lp.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) c !["](backquote.gif) ![{](lbrace.gif) ![n](_n.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
27 | 18, 26 | eqeltrri 2424 |
. . . . . 6
![{](lbrace.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
28 | | breq1 4642 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) c
0c c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | breq2 4643 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) c c 0c![)](rp.gif) ![)](rp.gif) |
30 | 28, 29 | orbi12d 690 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) c c ![a](_a.gif) 0c c c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | imbi2d 307 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) Nn 0c c c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | breq1 4642 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | breq2 4643 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c
c ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 32, 33 | orbi12d 690 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
c c ![a](_a.gif) ![(](lp.gif) c c ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | breq1 4642 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c ![(](lp.gif) 1c c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | breq2 4643 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 36, 37 | orbi12d 690 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) c c ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | breq1 4642 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | breq2 4643 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) c
c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 40, 41 | orbi12d 690 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
c c ![a](_a.gif) ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | imbi2d 307 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | nnnc 6146 |
. . . . . . . 8
![(](lp.gif) Nn NC ![)](rp.gif) |
45 | | le0nc 6200 |
. . . . . . . 8
![(](lp.gif) NC 0c c ![n](_n.gif) ![)](rp.gif) |
46 | 44, 45 | syl 15 |
. . . . . . 7
![(](lp.gif) Nn 0c c ![n](_n.gif) ![)](rp.gif) |
47 | | orc 374 |
. . . . . . 7
0c c 0c c c
0c![)](rp.gif) ![)](rp.gif) |
48 | 46, 47 | syl 15 |
. . . . . 6
![(](lp.gif) Nn 0c c c 0c![)](rp.gif) ![)](rp.gif) |
49 | | nnnc 6146 |
. . . . . . . . 9
![(](lp.gif) Nn NC ![)](rp.gif) |
50 | | dflec2 6210 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![E.](exists.gif) NC ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | | nc0le1 6216 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) NC ![(](lp.gif) 0c 1c
c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | 1cnc 6139 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
NC |
53 | | le0nc 6200 |
. . . . . . . . . . . . . . . . . . . . . 22
1c NC 0c c 1c![)](rp.gif) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
0c c 1c |
55 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) 0c ![(](lp.gif) c
1c 0c c 1c![)](rp.gif) ![)](rp.gif) |
56 | 54, 55 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) 0c c 1c![)](rp.gif) |
57 | 56 | orim1i 503 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif)
0c 1c c ![p](_p.gif)
![(](lp.gif) c 1c 1c c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) 0c 1c c ![p](_p.gif) ![(](lp.gif) c 1c 1c c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 51, 58 | mpd 14 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) NC ![(](lp.gif) c
1c 1c c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | orcomd 377 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) NC 1c c c 1c![)](rp.gif) ![)](rp.gif) |
61 | 60 | adantl 452 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) NC NC 1c c c 1c![)](rp.gif) ![)](rp.gif) |
62 | | simpll 730 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
1c c ![p](_p.gif) NC ![)](rp.gif) |
63 | 52 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
1c c ![p](_p.gif) 1c
NC ![)](rp.gif) |
64 | | simplr 731 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
1c c ![p](_p.gif) NC ![)](rp.gif) |
65 | | simpr 447 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
1c c ![p](_p.gif) 1c
c ![p](_p.gif) ![)](rp.gif) |
66 | | leaddc2 6215 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC 1c NC NC
1c c ![p](_p.gif) ![(](lp.gif) 1c c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 62, 63, 64, 65, 66 | syl31anc 1185 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
1c c ![p](_p.gif) ![(](lp.gif) 1c c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 67 | ex 423 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) NC NC 1c c ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | | simpll 730 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC c 1c
NC ![)](rp.gif) |
70 | | simplr 731 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC c 1c
NC ![)](rp.gif) |
71 | 52 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC c 1c 1c NC ![)](rp.gif) |
72 | | simpr 447 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC c 1c c 1c![)](rp.gif) |
73 | | leaddc2 6215 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC 1c NC c
1c
![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
74 | 69, 70, 71, 72, 73 | syl31anc 1185 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC c 1c ![(](lp.gif)
![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
75 | 74 | ex 423 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c 1c ![(](lp.gif)
![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 68, 75 | orim12d 811 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c c c
1c
![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 61, 76 | mpd 14 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
78 | | breq2 4643 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) 1c c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | | breq1 4642 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 78, 79 | orbi12d 690 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
81 | 80 | biimprd 214 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 81 | com12 27 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![p](_p.gif) c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 77, 82 | syl 15 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 83 | rexlimdva 2738 |
. . . . . . . . . . . 12
![(](lp.gif) NC ![(](lp.gif) ![E.](exists.gif) NC ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 84 | adantr 451 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
NC ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 50, 85 | sylbid 206 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
87 | | addlecncs 6209 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) NC 1c NC c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
88 | 52, 87 | mpan2 652 |
. . . . . . . . . . . . . 14
![(](lp.gif) NC c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
89 | 88 | adantl 452 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC NC c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
90 | | peano2nc 6145 |
. . . . . . . . . . . . . . 15
![(](lp.gif) NC ![(](lp.gif)
1c
NC ![)](rp.gif) |
91 | 90 | adantl 452 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c
NC ![)](rp.gif) |
92 | | lectr 6211 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c NC ![(](lp.gif) ![(](lp.gif) c
c ![(](lp.gif) 1c![)](rp.gif)
c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
93 | 91, 92 | mpd3an3 1278 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 89, 93 | mpan2d 655 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
95 | 94 | ancoms 439 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | olc 373 |
. . . . . . . . . . 11
![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 95, 96 | syl6 29 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 86, 97 | jaod 369 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) c c ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 49, 44, 98 | syl2an 463 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) c c ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | ex 423 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) c c ![m](_m.gif) ![(](lp.gif) ![(](lp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 100 | a2d 23 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) c c ![m](_m.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | 27, 31, 35, 39, 43, 48, 101 | finds 4411 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) c
c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 102 | com12 27 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) c
c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | 4, 103 | vtoclga 2920 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 104 | com12 27 |
. 2
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 105 | imp 418 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |