Step | Hyp | Ref
| Expression |
1 | | iftrue 3668 |
. . . . . . . . 9
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
2 | 1 | eqcomd 2358 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | eleq1 2413 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![)](rp.gif) |
4 | | addceq1 4383 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
5 | | id 19 |
. . . . . . . . . . 11
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) |
6 | 3, 4, 5 | ifbieq12d 3684 |
. . . . . . . . . 10
![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | eqeq2d 2364 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | rspcev 2955 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![E.](exists.gif)
![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 2, 8 | sylan2 460 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
Nn ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | ancoms 439 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
12 | | 1cex 4142 |
. . . . . . . 8
1c
![_V](rmcv.gif) |
13 | 11, 12 | addcex 4394 |
. . . . . . 7
![(](lp.gif) 1c
![_V](rmcv.gif) |
14 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 14 | rexbidv 2635 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | df-phi 4565 |
. . . . . . 7
Phi ![{](lbrace.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
17 | 13, 15, 16 | elab2 2988 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
1c
Phi ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 10, 17 | sylibr 203 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) ![(](lp.gif) 1c Phi ![A](_ca.gif) ![)](rp.gif) |
19 | | eleq2 2414 |
. . . . . . . . 9
Phi
Phi
![(](lp.gif) ![(](lp.gif)
1c
Phi ![(](lp.gif) 1c Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | biimpac 472 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Phi Phi Phi ![B](_cb.gif) ![(](lp.gif) 1c Phi ![B](_cb.gif) ![)](rp.gif) |
21 | 14 | rexbidv 2635 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | df-phi 4565 |
. . . . . . . . . 10
Phi ![{](lbrace.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
23 | 13, 21, 22 | elab2 2988 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
Phi ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | iffalse 3669 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![y](_y.gif) ![)](rp.gif) |
25 | 24 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | biimpac 472 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif)
Nn ![(](lp.gif) 1c
![y](_y.gif) ![)](rp.gif) |
27 | | peano2 4403 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
28 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) 1c Nn Nn ![)](rp.gif) ![)](rp.gif) |
29 | 27, 28 | syl5ibcom 211 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c
Nn ![)](rp.gif) ![)](rp.gif) |
30 | 26, 29 | syl5 28 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) Nn Nn ![)](rp.gif) ![)](rp.gif) |
31 | 30 | expdimp 426 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![)](rp.gif) |
32 | 31 | pm2.18d 103 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) Nn ![)](rp.gif) |
33 | | simpl 443 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) Nn ![)](rp.gif) |
34 | | simpr 447 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | iftrue 3668 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
36 | 32, 35 | syl 15 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
37 | 34, 36 | eqtr2d 2386 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
38 | | peano4 4557 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) |
39 | 32, 33, 37, 38 | syl3anc 1182 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![z](_z.gif) ![)](rp.gif) |
40 | 39 | 3adant2 974 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
![z](_z.gif) ![)](rp.gif) |
41 | | simp2 956 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
![B](_cb.gif) ![)](rp.gif) |
42 | 40, 41 | eqeltrrd 2428 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
![B](_cb.gif) ![)](rp.gif) |
43 | 42 | 3expia 1153 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![B](_cb.gif) ![(](lp.gif) ![(](lp.gif) 1c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | rexlimdva 2738 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) 1c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 23, 44 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 20, 45 | syl5 28 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Phi Phi Phi ![B](_cb.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | exp3a 425 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c Phi Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | adantr 451 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) 1c
Phi Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 18, 48 | mpd 14 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | iffalse 3669 |
. . . . . . . . 9
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) |
51 | 50 | eqcomd 2358 |
. . . . . . . 8
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 6 | eqeq2d 2364 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 52 | rspcev 2955 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 51, 53 | sylan2 460 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
Nn ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 54 | ancoms 439 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | rexbidv 2635 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 11, 57, 16 | elab2 2988 |
. . . . . 6
![(](lp.gif) Phi ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 55, 58 | sylibr 203 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif)
Phi ![A](_ca.gif) ![)](rp.gif) |
60 | | eleq2 2414 |
. . . . . . . . 9
Phi
Phi
![(](lp.gif)
Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 60 | biimpac 472 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Phi Phi Phi ![B](_cb.gif) Phi ![B](_cb.gif) ![)](rp.gif) |
62 | 56 | rexbidv 2635 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 11, 62, 22 | elab2 2988 |
. . . . . . . . 9
![(](lp.gif) Phi ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
64 | | simpr 447 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 35 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | | peano2 4403 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
67 | | eleq1a 2422 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) |
68 | 66, 67 | syl 15 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) |
69 | 65, 68 | sylbid 206 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) Nn ![)](rp.gif) ![)](rp.gif) |
70 | 69 | com12 27 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![)](rp.gif) |
71 | 70 | con3d 125 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) Nn
Nn ![)](rp.gif) ![)](rp.gif) |
72 | 71 | impcom 419 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
73 | 72, 24 | syl 15 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![y](_y.gif) ![)](rp.gif) |
74 | 64, 73 | eqtr2d 2386 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif)
![z](_z.gif) ![)](rp.gif) |
75 | 74 | adantlr 695 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![B](_cb.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![z](_z.gif) ![)](rp.gif) |
76 | | simplr 731 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![B](_cb.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![B](_cb.gif) ![)](rp.gif) |
77 | 75, 76 | eqeltrrd 2428 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![B](_cb.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![B](_cb.gif) ![)](rp.gif) |
78 | 77 | ex 423 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![B](_cb.gif) ![(](lp.gif) ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 78 | rexlimdva 2738 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 63, 79 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) Phi
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
81 | 61, 80 | syl5 28 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Phi Phi Phi ![B](_cb.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 81 | exp3a 425 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) Phi Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 82 | adantr 451 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) ![(](lp.gif) Phi Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 59, 83 | mpd 14 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn ![A](_ca.gif) Phi Phi ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 49, 84 | pm2.61ian 765 |
. . 3
![(](lp.gif) Phi Phi
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 85 | com12 27 |
. 2
Phi
Phi
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 86 | ssrdv 3278 |
1
Phi
Phi
![B](_cb.gif) ![)](rp.gif) |