Proof of Theorem ax11
Step | Hyp | Ref
| Expression |
1 | | wal 134 |
. . . . . . . 8
![A.](forall.gif) ![:](colon.gif) ![(](lp.gif) ![(](lp.gif) ![*](hexstar.gif) ![*](hexstar.gif) ![)](rp.gif) |
2 | | ax11.1 |
. . . . . . . . 9
![A](_ca.gif) ![:](colon.gif) ![*](hexstar.gif) |
3 | 2 | wl 66 |
. . . . . . . 8
![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) |
4 | 1, 3 | wc 50 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
5 | 4 | id 25 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) |
6 | | wv 64 |
. . . . . . . . . 10
![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![:](colon.gif) ![al](_alpha.gif) |
7 | 3, 6 | wc 50 |
. . . . . . . . 9
![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
8 | 7 | wl 66 |
. . . . . . . 8
![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) |
9 | 3 | eta 178 |
. . . . . . . 8
![[](lbrack.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![]](rbrack.gif) |
10 | 1, 8, 9 | ceq2 90 |
. . . . . . 7
![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![]](rbrack.gif) |
11 | 4, 10 | a1i 28 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![]](rbrack.gif) |
12 | 5, 11 | mpbir 87 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | wim 137 |
. . . . . . . . 9
![:](colon.gif) ![(](lp.gif) ![(](lp.gif)
![*](hexstar.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | wv 64 |
. . . . . . . . . 10
![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![:](colon.gif) ![al](_alpha.gif) |
15 | 6, 14 | weqi 76 |
. . . . . . . . 9
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![:](colon.gif) ![*](hexstar.gif) |
16 | 13, 15, 2 | wov 72 |
. . . . . . . 8
![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![:](colon.gif) ![*](hexstar.gif) |
17 | 16 | wl 66 |
. . . . . . 7
![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) |
18 | 1, 17 | wc 50 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
19 | 1, 8 | wc 50 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
20 | 19 | id 25 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 15, 4 | simpr 23 |
. . . . . . . . . . 11
![(](lp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif)
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) |
22 | 21 | ax-cb1 29 |
. . . . . . . . . . . 12
![(](lp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif)
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
23 | 22, 10 | a1i 28 |
. . . . . . . . . . 11
![(](lp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif)
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![]](rbrack.gif) |
24 | 21, 23 | mpbir 87 |
. . . . . . . . . 10
![(](lp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif)
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | ax-cb2 30 |
. . . . . . . . 9
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
26 | 13, 25, 18 | wov 72 |
. . . . . . . 8
![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) ![:](colon.gif) ![*](hexstar.gif) |
27 | 7, 15 | simpl 22 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) |
28 | 7, 15 | simpr 23 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) |
29 | 3, 6, 28 | ceq2 90 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![]](rbrack.gif) |
30 | 7, 15 | wct 48 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
31 | 2 | beta 92 |
. . . . . . . . . . . . . . 15
![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) |
32 | 30, 31 | a1i 28 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) |
33 | 7, 29, 32 | eqtri 95 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) |
34 | 27, 33 | mpbi 82 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![A](_ca.gif) |
35 | 34 | ex 158 |
. . . . . . . . . . 11
![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif)
![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) |
36 | | wtru 43 |
. . . . . . . . . . 11
![T.](top.gif) ![:](colon.gif) ![*](hexstar.gif) |
37 | 35, 36 | adantl 56 |
. . . . . . . . . 10
![(](lp.gif) ![T.](top.gif)
![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) |
38 | 37 | ex 158 |
. . . . . . . . 9
![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![]](rbrack.gif) |
39 | 38 | alrimiv 151 |
. . . . . . . 8
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) |
40 | 7, 16 | ax5 207 |
. . . . . . . 8
![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) ![]](rbrack.gif) |
41 | 26, 39, 40 | mpd 156 |
. . . . . . 7
![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) |
42 | 19, 41 | a1i 28 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) |
43 | 18, 20, 42 | mpd 156 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) |
44 | 12, 43 | syl 16 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) |
45 | 36, 15 | wct 48 |
. . . 4
![(](lp.gif) ![T.](top.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif)
![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![)](rp.gif) ![:](colon.gif) ![*](hexstar.gif) |
46 | 44, 45 | adantl 56 |
. . 3
![(](lp.gif) ![(](lp.gif) ![T.](top.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) |
47 | 46 | ex 158 |
. 2
![(](lp.gif) ![T.](top.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif)
![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) |
48 | 47 | ex 158 |
1
![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![A](_ca.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![A](_ca.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) ![]](rbrack.gif) |