Step | Hyp | Ref
| Expression |
1 | | 0cnsuc 4401 |
. . . . . 6
![(](lp.gif) 1c 0c |
2 | | df-ne 2518 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
1c
0c ![(](lp.gif) 1c 0c![)](rp.gif) |
3 | 1, 2 | mpbi 199 |
. . . . 5
![(](lp.gif) 1c
0c |
4 | | iffalse 3669 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![y](_y.gif) ![)](rp.gif) |
5 | 4 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) Nn 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) 0c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 5 | biimpac 472 |
. . . . . . . . 9
![(](lp.gif) 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) Nn
0c
![y](_y.gif) ![)](rp.gif) |
7 | | peano1 4402 |
. . . . . . . . 9
0c
Nn |
8 | 6, 7 | syl6eqelr 2442 |
. . . . . . . 8
![(](lp.gif) 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) Nn Nn ![)](rp.gif) |
9 | 8 | ex 423 |
. . . . . . 7
0c ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
Nn Nn ![)](rp.gif) ![)](rp.gif) |
10 | 9 | pm2.18d 103 |
. . . . . 6
0c ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) Nn ![)](rp.gif) |
11 | | iftrue 3668 |
. . . . . . . . 9
![(](lp.gif) Nn ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
12 | 11 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) Nn 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) 0c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | eqcom 2355 |
. . . . . . . 8
0c ![(](lp.gif)
1c
![(](lp.gif) 1c
0c![)](rp.gif) |
14 | 12, 13 | syl6bb 252 |
. . . . . . 7
![(](lp.gif) Nn 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c
0c![)](rp.gif) ![)](rp.gif) |
15 | 14 | biimpd 198 |
. . . . . 6
![(](lp.gif) Nn 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif)
1c
0c![)](rp.gif) ![)](rp.gif) |
16 | 10, 15 | mpcom 32 |
. . . . 5
0c ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![(](lp.gif) 1c
0c![)](rp.gif) |
17 | 3, 16 | mto 167 |
. . . 4
0c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) |
18 | 17 | a1i 10 |
. . 3
![(](lp.gif) 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | nrex 2716 |
. 2
![E.](exists.gif)
0c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) |
20 | | 0cex 4392 |
. . 3
0c
![_V](rmcv.gif) |
21 | | eqeq1 2359 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif)
0c
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | rexbidv 2635 |
. . 3
![(](lp.gif) 0c ![(](lp.gif) ![E.](exists.gif) ![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![y](_y.gif) ![E.](exists.gif) 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | df-phi 4565 |
. . 3
Phi ![{](lbrace.gif) ![E.](exists.gif)
![if](_if.gif) ![(](lp.gif)
Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
24 | 20, 22, 23 | elab2 2988 |
. 2
0c
Phi ![E.](exists.gif) 0c ![if](_if.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 19, 24 | mtbir 290 |
1
0c
Phi ![A](_ca.gif) |