Step | Hyp | Ref
| Expression |
1 | | an4 797 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | simpl 443 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
3 | 2 | a1i 10 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | reeanv 2778 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Nn ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | addccom 4406 |
. . . . . . . . . 10
1c ![y](_y.gif)
![(](lp.gif) 1c![)](rp.gif) |
6 | | peano2 4403 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
7 | 5, 6 | syl5eqel 2437 |
. . . . . . . . 9
![(](lp.gif) Nn 1c ![y](_y.gif) Nn ![)](rp.gif) |
8 | | nncaddccl 4419 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn 1c ![y](_y.gif) Nn ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) Nn ![)](rp.gif) |
9 | 7, 8 | sylan2 460 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) Nn ![)](rp.gif) |
10 | 9 | adantl 452 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) Nn ![)](rp.gif) |
11 | | addceq1 4383 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | addceq1 4383 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
13 | 11, 12 | syl 15 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
14 | 13 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 14 | biimpa 470 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
16 | | addceq2 4384 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![(](lp.gif)
![z](_z.gif)
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | addcass 4415 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | addcass 4415 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 17, 18 | eqtri 2373 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
1c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 16, 19 | syl6eqr 2403 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![(](lp.gif)
![z](_z.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![x](_x.gif) 1c ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | addceq1 4383 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
22 | 20, 21 | syl 15 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) |
23 | 22 | eqeq2d 2364 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | rspcev 2955 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) |
25 | 24 | ex 423 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![y](_y.gif) ![)](rp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c
![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 10, 15, 25 | syl2im 34 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![x](_x.gif) 1c ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | rexlimdvva 2745 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![E.](exists.gif)
Nn ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 4, 27 | syl5bir 209 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 3, 28 | anim12d 546 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 1, 29 | syl5bi 208 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) 1c![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | opkltfing 4449 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | 3adant3 975 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | opkltfing 4449 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 33 | 3adant1 973 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 32, 34 | anbi12d 691 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![(](lp.gif) ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
1c![)](rp.gif) ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | opkltfing 4449 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | 3adant2 974 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 30, 35, 37 | 3imtr4d 259 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) |