Step | Hyp | Ref
| Expression |
1 | | rexeq 2630 |
. . 3
![( (](lp.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
2 | 1 | dcbid 824 |
. 2
![( (](lp.gif)
DECID ![E. E.](exists.gif)
DECID ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | rexeq 2630 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | 3 | dcbid 824 |
. 2
![( (](lp.gif) DECID ![E. E.](exists.gif)
DECID ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | rexeq 2630 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 5 | dcbid 824 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) DECID ![E.
E.](exists.gif) DECID ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | rexeq 2630 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 7 | dcbid 824 |
. 2
![( (](lp.gif) DECID ![E. E.](exists.gif)
DECID ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | rex0 3385 |
. . . . 5
![E. E.](exists.gif)
![ph ph](_varphi.gif) |
10 | 9 | olci 722 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
11 | | df-dc 821 |
. . . 4
DECID ![E. E.](exists.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
12 | 10, 11 | mpbir 145 |
. . 3
DECID ![E. E.](exists.gif) ![ph ph](_varphi.gif) |
13 | 12 | a1i 9 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif) DECID ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
14 | | simpr 109 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
15 | | sbsbc 2917 |
. . . . . . . . . 10
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[.
[.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
16 | | rexsns 3570 |
. . . . . . . . . 10
![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
17 | 15, 16 | bitr4i 186 |
. . . . . . . . 9
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
18 | 14, 17 | sylib 121 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
19 | 18 | olcd 724 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
20 | | rexun 3261 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
21 | 19, 20 | sylibr 133 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
22 | 21 | orcd 723 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | | df-dc 821 |
. . . . 5
DECID ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
24 | 22, 23 | sylibr 133 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
DECID ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
25 | | simpr 109 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) |
26 | 25 | orcd 723 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 26, 20 | sylibr 133 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
28 | 27 | orcd 723 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 28, 23 | sylibr 133 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) DECID ![E. E.](exists.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
30 | | simpr 109 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
31 | | simpr 109 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
32 | 17 | notbii 658 |
. . . . . . . . . . 11
![( (](lp.gif) ![[
[](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
33 | 31, 32 | sylib 121 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
34 | 33 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
35 | | ioran 742 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
36 | 30, 34, 35 | sylanbrc 414 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
37 | 20 | notbii 658 |
. . . . . . . 8
![( (](lp.gif) ![E.
E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 36, 37 | sylibr 133 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
39 | 38 | olcd 724 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 39, 23 | sylibr 133 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A.
A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) DECID ![E. E.](exists.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
41 | | exmiddc 822 |
. . . . . 6
DECID ![E. E.](exists.gif)
![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 41 | ad2antlr 481 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 29, 40, 42 | mpjaodan 788 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID
![E. E.](exists.gif)
![ph ph](_varphi.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
DECID ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
44 | | simplrr 526 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) |
45 | 44 | eldifad 3087 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif) ![A A](_ca.gif) ![) )](rp.gif) |
46 | | simp-4r 532 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif) ![A. A.](forall.gif)
DECID ![ph ph](_varphi.gif) ![) )](rp.gif) |
47 | | nfs1v 1913 |
. . . . . . . 8
![F/ F/](finv.gif) ![x x](_x.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) |
48 | 47 | nfdc 1638 |
. . . . . . 7
![F/ F/](finv.gif) DECID ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) |
49 | | sbequ12 1745 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 49 | dcbid 824 |
. . . . . . 7
![( (](lp.gif) DECID
DECID ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 48, 50 | rspc 2787 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID DECID ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 45, 46, 51 | sylc 62 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif)
DECID ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
53 | | exmiddc 822 |
. . . . 5
DECID ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 52, 53 | syl 14 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 24, 43, 54 | mpjaodan 788 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
DECID
![ph ph](_varphi.gif)
![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif)
DECID ![E. E.](exists.gif) ![ph
ph](_varphi.gif)
DECID ![E. E.](exists.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
56 | 55 | ex 114 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A. A.](forall.gif)
DECID ![ph ph](_varphi.gif) ![Fin Fin](_fin.gif) ![( (](lp.gif)
![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) DECID ![E.
E.](exists.gif) DECID ![E. E.](exists.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
57 | | simpl 108 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif) ![Fin Fin](_fin.gif) ![) )](rp.gif) |
58 | 2, 4, 6, 8, 13, 56, 57 | findcard2sd 6794 |
1
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) DECID ![ph ph](_varphi.gif) DECID ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |