Proof of Theorem ax11
Step | Hyp | Ref
| Expression |
1 | | wal 124 |
. . . . . . . 8
|
2 | | ax11.1 |
. . . . . . . . 9
|
3 | 2 | wl 59 |
. . . . . . . 8
|
4 | 1, 3 | wc 45 |
. . . . . . 7
|
5 | 4 | id 25 |
. . . . . 6
|
6 | | wv 58 |
. . . . . . . . . 10
|
7 | 3, 6 | wc 45 |
. . . . . . . . 9
|
8 | 7 | wl 59 |
. . . . . . . 8
|
9 | 3 | eta 166 |
. . . . . . . 8
|
10 | 1, 8, 9 | ceq2 80 |
. . . . . . 7
|
11 | 4, 10 | a1i 28 |
. . . . . 6
|
12 | 5, 11 | mpbir 77 |
. . . . 5
|
13 | | wim 127 |
. . . . . . . . 9
|
14 | | wv 58 |
. . . . . . . . . 10
|
15 | 6, 14 | weqi 68 |
. . . . . . . . 9
|
16 | 13, 15, 2 | wov 64 |
. . . . . . . 8
|
17 | 16 | wl 59 |
. . . . . . 7
|
18 | 1, 17 | wc 45 |
. . . . . 6
|
19 | 1, 8 | wc 45 |
. . . . . . 7
|
20 | 19 | id 25 |
. . . . . 6
|
21 | 15, 4 | simpr 23 |
. . . . . . . . . . 11
|
22 | 21 | ax-cb1 29 |
. . . . . . . . . . . 12
|
23 | 22, 10 | a1i 28 |
. . . . . . . . . . 11
|
24 | 21, 23 | mpbir 77 |
. . . . . . . . . 10
|
25 | 24 | ax-cb2 30 |
. . . . . . . . 9
|
26 | 13, 25, 18 | wov 64 |
. . . . . . . 8
|
27 | 7, 15 | simpl 22 |
. . . . . . . . . . . . 13
|
28 | 7, 15 | simpr 23 |
. . . . . . . . . . . . . . 15
|
29 | 3, 6, 28 | ceq2 80 |
. . . . . . . . . . . . . 14
|
30 | 7, 15 | wct 44 |
. . . . . . . . . . . . . . 15
|
31 | 2 | beta 82 |
. . . . . . . . . . . . . . 15
|
32 | 30, 31 | a1i 28 |
. . . . . . . . . . . . . 14
|
33 | 7, 29, 32 | eqtri 85 |
. . . . . . . . . . . . 13
|
34 | 27, 33 | mpbi 72 |
. . . . . . . . . . . 12
|
35 | 34 | ex 148 |
. . . . . . . . . . 11
|
36 | | wtru 40 |
. . . . . . . . . . 11
|
37 | 35, 36 | adantl 51 |
. . . . . . . . . 10
|
38 | 37 | ex 148 |
. . . . . . . . 9
|
39 | 38 | alrimiv 141 |
. . . . . . . 8
|
40 | 7, 16 | ax5 194 |
. . . . . . . 8
|
41 | 26, 39, 40 | mpd 146 |
. . . . . . 7
|
42 | 19, 41 | a1i 28 |
. . . . . 6
|
43 | 18, 20, 42 | mpd 146 |
. . . . 5
|
44 | 12, 43 | syl 16 |
. . . 4
|
45 | 36, 15 | wct 44 |
. . . 4
|
46 | 44, 45 | adantl 51 |
. . 3
|
47 | 46 | ex 148 |
. 2
|
48 | 47 | ex 148 |
1
|