Step | Hyp | Ref
| Expression |
1 | | dflec2 6210 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![E.](exists.gif) NC ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | tccl 6160 |
. . . . . . . 8
![(](lp.gif) NC Tc NC ![)](rp.gif) |
3 | | tccl 6160 |
. . . . . . . 8
![(](lp.gif) NC Tc NC ![)](rp.gif) |
4 | | addlecncs 6209 |
. . . . . . . 8
![(](lp.gif) Tc NC Tc
NC Tc c
Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 3, 4 | syl2an 463 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC NC Tc c
Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | tcdi 6164 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC NC Tc ![(](lp.gif)
![p](_p.gif)
Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | breqtrrd 4665 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC NC Tc c Tc ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | tceq 6158 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
Tc
Tc ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | breq2d 4651 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
Tc c Tc Tc c Tc ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 7, 9 | syl5ibrcom 213 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
Tc c Tc ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | rexlimdva 2738 |
. . . 4
![(](lp.gif) NC ![(](lp.gif) ![E.](exists.gif) NC ![(](lp.gif)
![p](_p.gif) Tc c Tc
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | adantr 451 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
NC ![(](lp.gif) ![p](_p.gif) Tc c Tc ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 1, 12 | sylbid 206 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c Tc c Tc ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | tccl 6160 |
. . . 4
![(](lp.gif) NC Tc NC ![)](rp.gif) |
15 | | dflec2 6210 |
. . . 4
![(](lp.gif) Tc NC Tc
NC Tc c Tc ![E.](exists.gif) NC Tc
Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 2, 14, 15 | syl2an 463 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC Tc c Tc ![E.](exists.gif) NC Tc
Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | simplr 731 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif)
NC ![)](rp.gif) |
18 | | simpll 730 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif)
NC ![)](rp.gif) |
19 | | simprl 732 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif)
NC ![)](rp.gif) |
20 | | simprr 733 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) Tc
Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | taddc 6229 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc
Tc ![p](_p.gif) ![)](rp.gif) ![E.](exists.gif) NC Tc ![q](_q.gif) ![)](rp.gif) |
22 | 17, 18, 19, 20, 21 | syl31anc 1185 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
NC Tc ![q](_q.gif) ![)](rp.gif) |
23 | | addceq2 4384 |
. . . . . . . . . . . . 13
![(](lp.gif) Tc Tc ![p](_p.gif) Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | eqeq2d 2364 |
. . . . . . . . . . . 12
![(](lp.gif) Tc Tc
Tc ![p](_p.gif) Tc
Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | biimpac 472 |
. . . . . . . . . . 11
![(](lp.gif) Tc Tc ![p](_p.gif)
Tc ![q](_q.gif) Tc Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | tcdi 6164 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC Tc ![(](lp.gif)
![q](_q.gif)
Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | adantlr 695 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc
![(](lp.gif) ![q](_q.gif) Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | eqeq2d 2364 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc Tc ![(](lp.gif)
![q](_q.gif) Tc Tc Tc ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | simplr 731 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC
NC ![)](rp.gif) |
30 | | ncaddccl 6144 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![q](_q.gif) NC ![)](rp.gif) |
31 | 30 | adantlr 695 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![q](_q.gif)
NC ![)](rp.gif) |
32 | | tc11 6228 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ![q](_q.gif)
NC Tc
Tc ![(](lp.gif)
![q](_q.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 29, 31, 32 | syl2anc 642 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc Tc ![(](lp.gif)
![q](_q.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | addlecncs 6209 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) NC NC c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | breq2 4643 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![(](lp.gif) c c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 34, 35 | syl5ibrcom 213 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | adantlr 695 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![(](lp.gif) ![q](_q.gif) c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 33, 37 | sylbid 206 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc Tc ![(](lp.gif)
![q](_q.gif) c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 28, 38 | sylbird 226 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc Tc Tc ![q](_q.gif)
c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 25, 39 | syl5 28 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
Tc Tc ![p](_p.gif)
Tc ![q](_q.gif)
c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | expdimp 426 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC
NC Tc
Tc ![p](_p.gif) ![)](rp.gif) ![(](lp.gif) Tc c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 41 | an32s 779 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC Tc Tc ![p](_p.gif) ![)](rp.gif) NC ![(](lp.gif) Tc c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | rexlimdva 2738 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC Tc
Tc ![p](_p.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) NC Tc c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | adantrl 696 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) NC Tc c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 22, 44 | mpd 14 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC Tc Tc ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) c ![N](_cn.gif) ![)](rp.gif) |
46 | 45 | expr 598 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC Tc Tc ![p](_p.gif)
c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | rexlimdva 2738 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
NC Tc Tc ![p](_p.gif)
c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 16, 47 | sylbid 206 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC Tc c Tc c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 13, 48 | impbid 183 |
1
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c Tc c Tc
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |