Proof of Theorem cdlemk7u
Step | Hyp | Ref
| Expression |
1 | | simp31 1097 |
. . . 4
|
2 | | simp33 1099 |
. . . 4
|
3 | 1, 2 | jca 554 |
. . 3
|
4 | | cdlemk1.b |
. . . 4
|
5 | | cdlemk1.l |
. . . 4
|
6 | | cdlemk1.j |
. . . 4
|
7 | | cdlemk1.m |
. . . 4
|
8 | | cdlemk1.a |
. . . 4
|
9 | | cdlemk1.h |
. . . 4
|
10 | | cdlemk1.t |
. . . 4
|
11 | | cdlemk1.r |
. . . 4
|
12 | | cdlemk1.s |
. . . 4
|
13 | | cdlemk1.o |
. . . 4
|
14 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | cdlemk6u 36150 |
. . 3
|
15 | 3, 14 | syld3an3 1371 |
. 2
|
16 | | simp11l 1172 |
. . . . 5
|
17 | | simp11r 1173 |
. . . . 5
|
18 | 16, 17 | jca 554 |
. . . 4
|
19 | | simp23 1096 |
. . . 4
|
20 | | simp212 1200 |
. . . 4
|
21 | | simp12 1092 |
. . . . 5
|
22 | | simp13 1093 |
. . . . 5
|
23 | | simp211 1199 |
. . . . 5
|
24 | 21, 22, 23 | 3jca 1242 |
. . . 4
|
25 | | simp331 1214 |
. . . . 5
|
26 | | simp332 1215 |
. . . . . 6
|
27 | 26 | necomd 2849 |
. . . . 5
|
28 | 25, 27 | jca 554 |
. . . 4
|
29 | | simp311 1208 |
. . . . 5
|
30 | | simp313 1210 |
. . . . 5
|
31 | | simp312 1209 |
. . . . 5
|
32 | 29, 30, 31 | 3jca 1242 |
. . . 4
|
33 | | simp22 1095 |
. . . 4
|
34 | | cdlemk1.u |
. . . . 5
|
35 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuv2 36155 |
. . . 4
|
36 | 18, 19, 20, 24, 28, 32, 33, 35 | syl313anc 1350 |
. . 3
|
37 | 5, 6, 8, 9, 10, 11 | trljat1 35453 |
. . . . 5
|
38 | 18, 20, 33, 37 | syl3anc 1326 |
. . . 4
|
39 | 38 | oveq1d 6665 |
. . 3
|
40 | 36, 39 | eqtrd 2656 |
. 2
|
41 | | hllat 34650 |
. . . . 5
|
42 | 16, 41 | syl 17 |
. . . 4
|
43 | | simp213 1201 |
. . . . . 6
|
44 | | simp333 1216 |
. . . . . . . 8
|
45 | 44 | necomd 2849 |
. . . . . . 7
|
46 | 25, 45 | jca 554 |
. . . . . 6
|
47 | | simp32 1098 |
. . . . . . 7
|
48 | 29, 47, 31 | 3jca 1242 |
. . . . . 6
|
49 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuat 36154 |
. . . . . 6
|
50 | 18, 19, 43, 24, 46, 48, 33, 49 | syl313anc 1350 |
. . . . 5
|
51 | 4, 8 | atbase 34576 |
. . . . 5
|
52 | 50, 51 | syl 17 |
. . . 4
|
53 | | simp22l 1180 |
. . . . 5
|
54 | | cdlemk1.v |
. . . . . 6
|
55 | 4, 5, 6, 8, 9, 10,
11, 7, 54 | cdlemkvcl 36130 |
. . . . 5
|
56 | 16, 17, 22, 20, 43, 53, 55 | syl231anc 1346 |
. . . 4
|
57 | 4, 6 | latjcom 17059 |
. . . 4
|
58 | 42, 52, 56, 57 | syl3anc 1326 |
. . 3
|
59 | 54 | a1i 11 |
. . . 4
|
60 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 34 | cdlemkuv2 36155 |
. . . . . 6
|
61 | 18, 19, 43, 24, 46, 48, 33, 60 | syl313anc 1350 |
. . . . 5
|
62 | 5, 6, 8, 9, 10, 11 | trljat1 35453 |
. . . . . . . 8
|
63 | 18, 43, 33, 62 | syl3anc 1326 |
. . . . . . 7
|
64 | 5, 8, 9, 10 | ltrnat 35426 |
. . . . . . . . 9
|
65 | 18, 43, 53, 64 | syl3anc 1326 |
. . . . . . . 8
|
66 | 6, 8 | hlatjcom 34654 |
. . . . . . . 8
|
67 | 16, 65, 53, 66 | syl3anc 1326 |
. . . . . . 7
|
68 | 63, 67 | eqtr4d 2659 |
. . . . . 6
|
69 | | simp1 1061 |
. . . . . . . 8
|
70 | 23, 33, 19 | 3jca 1242 |
. . . . . . . 8
|
71 | 29, 31, 25 | 3jca 1242 |
. . . . . . . 8
|
72 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | cdlemkoatnle 36139 |
. . . . . . . . 9
|
73 | 72 | simpld 475 |
. . . . . . . 8
|
74 | 69, 70, 71, 73 | syl3anc 1326 |
. . . . . . 7
|
75 | 43, 22 | jca 554 |
. . . . . . . 8
|
76 | 8, 9, 10, 11 | trlcocnvat 36012 |
. . . . . . . 8
|
77 | 18, 75, 44, 76 | syl3anc 1326 |
. . . . . . 7
|
78 | 6, 8 | hlatjcom 34654 |
. . . . . . 7
|
79 | 16, 74, 77, 78 | syl3anc 1326 |
. . . . . 6
|
80 | 68, 79 | oveq12d 6668 |
. . . . 5
|
81 | 61, 80 | eqtrd 2656 |
. . . 4
|
82 | 59, 81 | oveq12d 6668 |
. . 3
|
83 | 58, 82 | eqtrd 2656 |
. 2
|
84 | 15, 40, 83 | 3brtr4d 4685 |
1
|