Proof of Theorem sbcomxyyz
Step | Hyp | Ref
| Expression |
1 | | ax-bndl 1487 |
. 2
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
2 | | ax-ial 1515 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![z z](_z.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![) )](rp.gif) |
3 | | drsb1 1772 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
4 | 2, 3 | sbbidh 1818 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | drsb1 1772 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 4, 5 | bitr3d 189 |
. . 3
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | sbequ12 1745 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 7 | sps 1518 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | hbae 1697 |
. . . . . 6
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![) )](rp.gif) |
10 | | sbequ12 1745 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 10 | sps 1518 |
. . . . . 6
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 9, 11 | sbbidh 1818 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 8, 12 | bitr3d 189 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | df-nf 1438 |
. . . . . 6
![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) |
15 | 14 | albii 1447 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | | ax-ial 1515 |
. . . . . . 7
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![y y](_y.gif) ![) )](rp.gif) |
17 | | nfs1v 1913 |
. . . . . . . . . 10
![F/ F/](finv.gif) ![x x](_x.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) |
18 | 17 | nfsb 1920 |
. . . . . . . . 9
![F/ F/](finv.gif) ![x x](_x.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) |
19 | 18 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![F/ F/](finv.gif) ![x x](_x.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
20 | 19 | nfrd 1501 |
. . . . . . 7
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | nfr 1499 |
. . . . . . . . 9
![( (](lp.gif) ![F/ F/](finv.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) |
22 | | nfnf1 1524 |
. . . . . . . . . . . . 13
![F/ F/](finv.gif) ![z z](_z.gif) ![F/ F/](finv.gif) ![y y](_y.gif) |
23 | | nfa1 1522 |
. . . . . . . . . . . . 13
![F/ F/](finv.gif) ![z z](_z.gif) ![A. A.](forall.gif) ![y y](_y.gif) |
24 | 22, 23 | nfan 1545 |
. . . . . . . . . . . 12
![F/ F/](finv.gif) ![z z](_z.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![)
)](rp.gif) |
25 | 24 | nfri 1500 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | | nfs1v 1913 |
. . . . . . . . . . . . 13
![F/ F/](finv.gif) ![z z](_z.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) |
27 | 26 | a1i 9 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![F/ F/](finv.gif) ![z z](_z.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
28 | 27 | nfrd 1501 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | | sbequ12 1745 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 29, 7 | sylan9bb 458 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![y y](_y.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 30 | ex 114 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 31 | sps 1518 |
. . . . . . . . . . . 12
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 32 | adantl 275 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 25, 28, 33 | sbiedh 1761 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 34 | ex 114 |
. . . . . . . . 9
![( (](lp.gif) ![F/ F/](finv.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 21, 35 | syld 45 |
. . . . . . . 8
![( (](lp.gif) ![F/ F/](finv.gif) ![( (](lp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 36 | sps 1518 |
. . . . . . 7
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![( (](lp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 16, 20, 37 | sbiedh 1761 |
. . . . . 6
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 38 | bicomd 140 |
. . . . 5
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![F/ F/](finv.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 15, 39 | sylbir 134 |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![z
z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 13, 40 | jaoi 706 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![( (](lp.gif)
![A. A.](forall.gif)
![y y](_y.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 6, 41 | jaoi 706 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 1, 42 | ax-mp 5 |
1
![( (](lp.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![z z](_z.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |