Step | Hyp | Ref
| Expression |
1 | | 3dim0.j |
. . . 4
|
2 | | 3dim0.l |
. . . 4
|
3 | | 3dim0.a |
. . . 4
|
4 | 1, 2, 3 | 3dim0 34743 |
. . 3
|
5 | 4 | adantr 481 |
. 2
|
6 | | simpl2 1065 |
. . . . . . . . . . 11
|
7 | 1, 2, 3 | 3dimlem1 34744 |
. . . . . . . . . . . 12
|
8 | 7 | 3ad2antl3 1225 |
. . . . . . . . . . 11
|
9 | 1, 2, 3 | 3dim1lem5 34752 |
. . . . . . . . . . 11
|
10 | 6, 8, 9 | syl2anc 693 |
. . . . . . . . . 10
|
11 | | simp13 1093 |
. . . . . . . . . . . . . 14
|
12 | | simp22 1095 |
. . . . . . . . . . . . . 14
|
13 | | simp23 1096 |
. . . . . . . . . . . . . 14
|
14 | 11, 12, 13 | 3jca 1242 |
. . . . . . . . . . . . 13
|
15 | 14 | ad2antrr 762 |
. . . . . . . . . . . 12
|
16 | | simpll1 1100 |
. . . . . . . . . . . . 13
|
17 | | simp21 1094 |
. . . . . . . . . . . . . . 15
|
18 | | simp32 1098 |
. . . . . . . . . . . . . . 15
|
19 | | simp33 1099 |
. . . . . . . . . . . . . . 15
|
20 | 17, 18, 19 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
21 | 20 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
22 | | simplr 792 |
. . . . . . . . . . . . 13
|
23 | | simpr 477 |
. . . . . . . . . . . . 13
|
24 | 1, 2, 3 | 3dimlem2 34745 |
. . . . . . . . . . . . 13
|
25 | 16, 21, 22, 23, 24 | syl112anc 1330 |
. . . . . . . . . . . 12
|
26 | 1, 2, 3 | 3dim1lem5 34752 |
. . . . . . . . . . . 12
|
27 | 15, 25, 26 | syl2anc 693 |
. . . . . . . . . . 11
|
28 | 11, 17, 13 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
29 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
30 | | simp1 1061 |
. . . . . . . . . . . . . . . . 17
|
31 | 17, 12 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
32 | | simp31 1097 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32, 19 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
34 | 30, 31, 33 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
36 | | simplrl 800 |
. . . . . . . . . . . . . . 15
|
37 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
38 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
39 | 1, 2, 3 | 3dimlem3 34747 |
. . . . . . . . . . . . . . 15
|
40 | 35, 36, 37, 38, 39 | syl13anc 1328 |
. . . . . . . . . . . . . 14
|
41 | 1, 2, 3 | 3dim1lem5 34752 |
. . . . . . . . . . . . . 14
|
42 | 29, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . 13
|
43 | 11, 17, 12 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
44 | 43 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
45 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
|
46 | | simpl21 1139 |
. . . . . . . . . . . . . . . . . 18
|
47 | | simpl22 1140 |
. . . . . . . . . . . . . . . . . 18
|
48 | 46, 47 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
49 | | simpl31 1142 |
. . . . . . . . . . . . . . . . . 18
|
50 | | simpl32 1143 |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 50 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
52 | 45, 48, 51 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . 15
|
54 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
55 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
56 | 1, 2, 3 | 3dimlem4 34750 |
. . . . . . . . . . . . . . 15
|
57 | 53, 54, 55, 56 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
58 | 1, 2, 3 | 3dim1lem5 34752 |
. . . . . . . . . . . . . 14
|
59 | 44, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . 13
|
60 | 42, 59 | pm2.61dan 832 |
. . . . . . . . . . . 12
|
61 | 60 | anassrs 680 |
. . . . . . . . . . 11
|
62 | 27, 61 | pm2.61dan 832 |
. . . . . . . . . 10
|
63 | 10, 62 | pm2.61dane 2881 |
. . . . . . . . 9
|
64 | 63 | 3exp 1264 |
. . . . . . . 8
|
65 | 64 | 3expd 1284 |
. . . . . . 7
|
66 | 65 | 3exp 1264 |
. . . . . 6
|
67 | 66 | imp43 621 |
. . . . 5
|
68 | 67 | impd 447 |
. . . 4
|
69 | 68 | rexlimdvv 3037 |
. . 3
|
70 | 69 | rexlimdvva 3038 |
. 2
|
71 | 5, 70 | mpd 15 |
1
|