Step | Hyp | Ref
| Expression |
1 | | opklefing 4448 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | 1 | 3adant3 975 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![E.](exists.gif) Nn ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | addcnnul 4453 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | simpld 445 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
5 | 4 | a1i 10 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | nncaddccl 4419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![y](_y.gif) Nn ![)](rp.gif) |
7 | 6 | 3adant1 973 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![y](_y.gif) Nn ![)](rp.gif) |
8 | | addcass 4415 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | addceq1 4383 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![)](rp.gif)
1c![)](rp.gif) |
11 | 10 | a1i 10 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
12 | | addceq2 4384 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | addceq1 4383 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
14 | 12, 13 | syl 15 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
15 | 14 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | rspcev 2955 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![)](rp.gif) 1c![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
1c![)](rp.gif) ![)](rp.gif) |
17 | 7, 11, 16 | syl2anc 642 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) |
18 | | eqeq1 2359 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif)
1c
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | rexbidv 2635 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif)
1c
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 17, 19 | syl5ibrcom 213 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif)
1c
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | 3expa 1151 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | adantllr 699 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn
Nn Nn ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | rexlimdva 2738 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 5, 23 | anim12d 546 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | addcexg 4393 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![x](_x.gif) ![_V](rmcv.gif) ![)](rp.gif) |
26 | 25 | adantlr 695 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif)
![x](_x.gif)
![_V](rmcv.gif) ![)](rp.gif) |
27 | | simplr 731 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn
Nn ![)](rp.gif) |
28 | | opkltfing 4449 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
Nn ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![C](_cc.gif) fin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 26, 27, 28 | syl2anc 642 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![C](_cc.gif) fin ![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | opkltfing 4449 |
. . . . . . . 8
![(](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) |
31 | 30 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](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) |
32 | 24, 29, 31 | 3imtr4d 259 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) |
33 | | opkeq1 4059 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![C](_cc.gif) ![>>](rrangle.gif) ![)](rp.gif) |
34 | 33 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif)
![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) |
35 | 34 | imbi1d 308 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![(](lp.gif) ![x](_x.gif) ![)](rp.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 32, 35 | syl5ibrcom 213 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif)
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | rexlimdva 2738 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 37 | 3adant2 974 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 2, 38 | sylbid 206 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![C](_cc.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![C](_cc.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 39 | imp3a 420 |
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) |