Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . 4
![_V](rmcv.gif) |
2 | | vex 2862 |
. . . 4
![_V](rmcv.gif) |
3 | 1, 2 | eqvinop 4606 |
. . 3
![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | 19.8a 1756 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | 19.8a 1756 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif)
![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 4, 5 | syl 15 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | ex 423 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | opth 4602 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif)
![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | anbi1i 676 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | 2exbii 1583 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | nfe1 1732 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![x](_x.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | nfae 1954 |
. . . . . . . . . . . . . 14
![F/ F/](finv.gif) ![y](_y.gif) ![A.](forall.gif)
![x](_x.gif) |
13 | | anass 630 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![(](lp.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | 19.8a 1756 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 14 | a1i 10 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![(](lp.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | anim2d 548 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 13, 16 | syl5bi 208 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![ph](_varphi.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 12, 17 | eximd 1770 |
. . . . . . . . . . . . 13
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | biidd 228 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | drex1 1967 |
. . . . . . . . . . . . 13
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 18, 20 | sylibd 205 |
. . . . . . . . . . . 12
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 13 | exbii 1582 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | 19.40 1609 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | nfnae 1956 |
. . . . . . . . . . . . . . . . . 18
![F/ F/](finv.gif) ![A.](forall.gif) ![x](_x.gif) |
25 | | dveeq2 1940 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![A.](forall.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 24, 25 | nfd 1766 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![A.](forall.gif)
![F/ F/](finv.gif) ![x](_x.gif) ![)](rp.gif) |
27 | 26 | 19.9d 1782 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | anim1d 547 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 23, 28 | syl5 28 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 22, 29 | syl5bi 208 |
. . . . . . . . . . . . 13
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | 19.8a 1756 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | syl6 29 |
. . . . . . . . . . . 12
![(](lp.gif) ![A.](forall.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 21, 32 | pm2.61i 156 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 11, 33 | exlimi 1803 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | euequ1 2292 |
. . . . . . . . . . . . . 14
![E!](_e1.gif)
![z](_z.gif) |
36 | | equcom 1680 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![x](_x.gif) ![)](rp.gif) |
37 | 36 | eubii 2213 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E!](_e1.gif) ![E!](_e1.gif) ![x](_x.gif) ![)](rp.gif) |
38 | 35, 37 | mpbi 199 |
. . . . . . . . . . . . 13
![E!](_e1.gif)
![x](_x.gif) |
39 | | eupick 2267 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![E!](_e1.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 38, 39 | mpan 651 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | com12 27 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | euequ1 2292 |
. . . . . . . . . . . . . 14
![E!](_e1.gif) ![w](_w.gif) |
43 | | equcom 1680 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![y](_y.gif) ![)](rp.gif) |
44 | 43 | eubii 2213 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E!](_e1.gif) ![E!](_e1.gif) ![y](_y.gif) ![)](rp.gif) |
45 | 42, 44 | mpbi 199 |
. . . . . . . . . . . . 13
![E!](_e1.gif) ![y](_y.gif) |
46 | | eupick 2267 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![E!](_e1.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 45, 46 | mpan 651 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![(](lp.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | com12 27 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 41, 48 | sylan9 638 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 34, 49 | syl5 28 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![ph](_varphi.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 10, 50 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 8, 51 | sylbi 187 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif)
![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 7, 52 | impbid 183 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | eqeq1 2359 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif)
![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![>.](rangle.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 54 | anbi1d 685 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif)
![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif)
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 55 | 2exbidv 1628 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | bibi2d 309 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 54, 57 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif) ![(](lp.gif)
![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![x](_x.gif)
![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 53, 58 | mpbiri 224 |
. . . . 5
![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![(](lp.gif)
![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | adantr 451 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 60 | exlimivv 1635 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![w](_w.gif) ![(](lp.gif) ![<.](langle.gif) ![z](_z.gif) ![w](_w.gif) ![<.](langle.gif) ![z](_z.gif)
![w](_w.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![>.](rangle.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | 3, 61 | sylbi 187 |
. 2
![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 62 | pm2.43i 43 |
1
![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<.](langle.gif) ![x](_x.gif) ![y](_y.gif) ![ph](_varphi.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |