Proof of Theorem 3vded3
Step | Hyp | Ref
| Expression |
1 | | df-i0 43 |
. 2
|
2 | | ax-a3 32 |
. . 3
|
3 | | cmtrcom 190 |
. . . . . . . . . . . . . . . 16
|
4 | 3 | lor 70 |
. . . . . . . . . . . . . . 15
|
5 | | df-i0 43 |
. . . . . . . . . . . . . . 15
|
6 | | df-i0 43 |
. . . . . . . . . . . . . . 15
|
7 | 4, 5, 6 | 3tr1 63 |
. . . . . . . . . . . . . 14
|
8 | | 3vded3.1 |
. . . . . . . . . . . . . 14
|
9 | 7, 8 | ax-r2 36 |
. . . . . . . . . . . . 13
|
10 | 9 | i0cmtrcom 495 |
. . . . . . . . . . . 12
|
11 | 10 | comcom4 455 |
. . . . . . . . . . 11
|
12 | 11 | comcom 453 |
. . . . . . . . . 10
|
13 | | comid 187 |
. . . . . . . . . . 11
|
14 | 13 | comcom3 454 |
. . . . . . . . . 10
|
15 | 12, 14 | fh1 469 |
. . . . . . . . 9
|
16 | | df-i0 43 |
. . . . . . . . . . . 12
|
17 | 16 | ax-r1 35 |
. . . . . . . . . . 11
|
18 | | 3vded3.2 |
. . . . . . . . . . 11
|
19 | 17, 18 | ax-r2 36 |
. . . . . . . . . 10
|
20 | 19 | lan 77 |
. . . . . . . . 9
|
21 | | dff 101 |
. . . . . . . . . . . . 13
|
22 | | ancom 74 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | ax-r2 36 |
. . . . . . . . . . . 12
|
24 | 23 | lor 70 |
. . . . . . . . . . 11
|
25 | 24 | ax-r1 35 |
. . . . . . . . . 10
|
26 | | or0 102 |
. . . . . . . . . 10
|
27 | 25, 26 | ax-r2 36 |
. . . . . . . . 9
|
28 | 15, 20, 27 | 3tr2 64 |
. . . . . . . 8
|
29 | | an1 106 |
. . . . . . . 8
|
30 | | ancom 74 |
. . . . . . . 8
|
31 | 28, 29, 30 | 3tr2 64 |
. . . . . . 7
|
32 | 31 | lor 70 |
. . . . . 6
|
33 | | orabs 120 |
. . . . . 6
|
34 | 32, 33 | ax-r2 36 |
. . . . 5
|
35 | 34 | ax-r5 38 |
. . . 4
|
36 | 35 | ax-r1 35 |
. . 3
|
37 | | df-i0 43 |
. . . 4
|
38 | | df-i0 43 |
. . . . 5
|
39 | 38 | lor 70 |
. . . 4
|
40 | 37, 39 | ax-r2 36 |
. . 3
|
41 | 2, 36, 40 | 3tr1 63 |
. 2
|
42 | | 3vded3.3 |
. 2
|
43 | 1, 41, 42 | 3tr 65 |
1
|