Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7737 |
. . . . . 6
![CC CC](bbc.gif) |
2 | | 1ap0 8376 |
. . . . . 6
# ![0 0](0.gif) |
3 | 1, 2 | div0api 8530 |
. . . . 5
![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) |
4 | | 0z 9089 |
. . . . . 6
![ZZ ZZ](bbz.gif) |
5 | | 1nn 8755 |
. . . . . 6
![NN NN](bbn.gif) |
6 | | znq 9443 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![1 1](1.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
7 | 4, 5, 6 | mp2an 423 |
. . . . 5
![( (](lp.gif) ![1 1](1.gif) ![QQ QQ](bbq.gif) |
8 | 3, 7 | eqeltrri 2214 |
. . . 4
![QQ QQ](bbq.gif) |
9 | | qapne 9458 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![QQ QQ](bbq.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 8, 9 | mpan2 422 |
. . 3
![( (](lp.gif) ![( (](lp.gif) #
![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
11 | 10 | biimpar 295 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) # ![0 0](0.gif) ![) )](rp.gif) |
12 | | elq 9441 |
. . . 4
![( (](lp.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | nnne0 8772 |
. . . . . . . 8
![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) |
14 | 13 | ancli 321 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | | nnz 9097 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
16 | | zapne 9149 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 15, 4, 16 | sylancl 410 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) #
![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 17 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 18 | pm5.32i 450 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 19 | anbi1i 454 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif)
![( (](lp.gif)
![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | breq1 3940 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![( (](lp.gif) #
![( (](lp.gif) ![y
y](_y.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | | zcn 9083 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
23 | | nncn 8752 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
24 | 22, 23 | anim12i 336 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | | divap0b 8467 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
# ![0 0](0.gif) ![( (](lp.gif) #
![( (](lp.gif) ![y y](_y.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | 3expa 1182 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![(
(](lp.gif) ![y y](_y.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 24, 26 | sylan 281 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![(
(](lp.gif) ![y y](_y.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 27 | bicomd 140 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) # # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 21, 28 | sylan9bbr 459 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) # # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 20, 29 | sylbir 134 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) # # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | simplll 523 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
32 | | zapne 9149 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 31, 4, 32 | sylancl 410 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 30, 33 | bitrd 187 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | zmulcl 9131 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![y y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
36 | 15, 35 | sylan2 284 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![y y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
37 | 36 | adantr 274 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif)
![( (](lp.gif) ![y y](_y.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
38 | | msqznn 9175 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(
(](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
39 | 38 | adantlr 469 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif)
![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![) )](rp.gif) |
40 | 37, 39 | jca 304 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 40 | adantlr 469 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![0 0](0.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![( (](lp.gif)
![x x](_x.gif) ![NN NN](bbn.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 41 | adantlr 469 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 20 | anbi1i 454 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) # ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 33 | pm5.32i 450 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) # ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 43, 44 | bitri 183 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) # ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | | oveq2 5790 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | | dividap 8485 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![x x](_x.gif) ![1 1](1.gif) ![) )](rp.gif) |
48 | 47 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![1 1](1.gif) ![) )](rp.gif) |
49 | 48 | oveq1d 5797 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![(
(](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | | simpll 519 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
51 | | simpl 108 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | | divdivdivap 8497 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![(
(](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 50, 51, 51, 52, 53 | syl22anc 1218 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![(
(](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 49, 54 | eqtr3d 2175 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 55 | an4s 578 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) # # ![0 0](0.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | 24, 56 | sylan 281 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) # # ![0 0](0.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 57 | anass1rs 561 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![(
(](lp.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 46, 58 | sylan9eqr 2195 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 59 | an32s 558 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) # ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![(
(](lp.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 45, 60 | sylbir 134 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![0 0](0.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 42, 61 | jca 304 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![(
(](lp.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
63 | 62 | ex 114 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![(
(](lp.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 34, 63 | sylbid 149 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif) ![( (](lp.gif) ![y
y](_y.gif) ![) )](rp.gif) ![(
(](lp.gif) # ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![(
(](lp.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 64 | ex 114 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![( (](lp.gif) #
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif)
![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 65 | anasss 397 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y
y](_y.gif) ![( (](lp.gif) #
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif)
![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 14, 66 | sylan2 284 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) # ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | | rspceov 5821 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif)
![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | 68 | 3expa 1182 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | | elq 9441 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 69, 70 | sylibr 133 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
72 | 67, 71 | syl8 71 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) # ![( (](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | 72 | rexlimivv 2558 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![y
y](_y.gif) ![( (](lp.gif) #
![( (](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | 12, 73 | sylbi 120 |
. . 3
![( (](lp.gif) ![( (](lp.gif) #
![( (](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 74 | imp 123 |
. 2
![( (](lp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![( (](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
76 | 11, 75 | syldan 280 |
1
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |