Proof of Theorem cdleme20l2
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. . . . 5
|
2 | | hllat 34650 |
. . . . 5
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | | simp11r 1173 |
. . . . 5
|
5 | | simp12l 1174 |
. . . . 5
|
6 | | simp13l 1176 |
. . . . 5
|
7 | | simp22l 1180 |
. . . . 5
|
8 | | cdleme19.l |
. . . . . 6
|
9 | | cdleme19.j |
. . . . . 6
|
10 | | cdleme19.m |
. . . . . 6
|
11 | | cdleme19.a |
. . . . . 6
|
12 | | cdleme19.h |
. . . . . 6
|
13 | | cdleme19.u |
. . . . . 6
|
14 | | cdleme19.f |
. . . . . 6
|
15 | | eqid 2622 |
. . . . . 6
|
16 | 8, 9, 10, 11, 12, 13, 14, 15 | cdleme1b 35513 |
. . . . 5
|
17 | 1, 4, 5, 6, 7, 16 | syl23anc 1333 |
. . . 4
|
18 | | simp21l 1178 |
. . . . 5
|
19 | | cdleme19.d |
. . . . . 6
|
20 | 8, 9, 10, 11, 12, 19, 15 | cdlemedb 35584 |
. . . . 5
|
21 | 1, 4, 18, 7, 20 | syl22anc 1327 |
. . . 4
|
22 | | simp23l 1182 |
. . . . 5
|
23 | | cdleme19.g |
. . . . . 6
|
24 | 8, 9, 10, 11, 12, 13, 23, 15 | cdleme1b 35513 |
. . . . 5
|
25 | 1, 4, 5, 6, 22, 24 | syl23anc 1333 |
. . . 4
|
26 | | cdleme19.y |
. . . . . 6
|
27 | 8, 9, 10, 11, 12, 26, 15 | cdlemedb 35584 |
. . . . 5
|
28 | 1, 4, 18, 22, 27 | syl22anc 1327 |
. . . 4
|
29 | 15, 9 | latj4 17101 |
. . . 4
|
30 | 3, 17, 21, 25, 28, 29 | syl122anc 1335 |
. . 3
|
31 | | simp1 1061 |
. . . . . 6
|
32 | | simp22 1095 |
. . . . . 6
|
33 | | simp23 1096 |
. . . . . 6
|
34 | | simp21 1094 |
. . . . . 6
|
35 | | simp31 1097 |
. . . . . 6
|
36 | | simp321 1211 |
. . . . . . 7
|
37 | | simp322 1212 |
. . . . . . 7
|
38 | 36, 37 | jca 554 |
. . . . . 6
|
39 | | simp323 1213 |
. . . . . 6
|
40 | | cdleme20.v |
. . . . . . 7
|
41 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20d 35600 |
. . . . . 6
|
42 | 31, 32, 33, 34, 35, 38, 39, 41 | syl133anc 1349 |
. . . . 5
|
43 | | simp22r 1181 |
. . . . . 6
|
44 | | simp31r 1185 |
. . . . . 6
|
45 | 8, 9, 10, 11, 12, 40 | lhpat2 35331 |
. . . . . 6
|
46 | 1, 4, 7, 43, 22, 44, 45 | syl222anc 1342 |
. . . . 5
|
47 | 42, 46 | eqeltrd 2701 |
. . . 4
|
48 | | simp11 1091 |
. . . . . . 7
|
49 | | simp12 1092 |
. . . . . . 7
|
50 | | simp13 1093 |
. . . . . . 7
|
51 | | simp31l 1184 |
. . . . . . 7
|
52 | 8, 9, 10, 11, 12, 13, 14 | cdleme3fa 35523 |
. . . . . . 7
|
53 | 48, 49, 50, 32, 51, 36, 52 | syl132anc 1344 |
. . . . . 6
|
54 | 8, 9, 10, 11, 12, 13, 23 | cdleme3fa 35523 |
. . . . . . 7
|
55 | 48, 49, 50, 33, 51, 37, 54 | syl132anc 1344 |
. . . . . 6
|
56 | | simp33r 1189 |
. . . . . . 7
|
57 | 8, 9, 10, 11, 12, 13, 14, 23 | cdleme16b 35566 |
. . . . . . 7
|
58 | 31, 32, 33, 35, 36, 37, 56, 57 | syl133anc 1349 |
. . . . . 6
|
59 | | eqid 2622 |
. . . . . . 7
|
60 | 9, 11, 59 | llni2 34798 |
. . . . . 6
|
61 | 1, 53, 55, 58, 60 | syl31anc 1329 |
. . . . 5
|
62 | 8, 9, 10, 11, 12, 19 | cdlemeda 35585 |
. . . . . . 7
|
63 | 1, 4, 7, 43, 18, 39, 36, 62 | syl223anc 1352 |
. . . . . 6
|
64 | | simp23r 1183 |
. . . . . . 7
|
65 | 8, 9, 10, 11, 12, 26 | cdlemeda 35585 |
. . . . . . 7
|
66 | 1, 4, 22, 64, 18, 39, 37, 65 | syl223anc 1352 |
. . . . . 6
|
67 | | simp32 1098 |
. . . . . . 7
|
68 | | simp33l 1188 |
. . . . . . 7
|
69 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20j 35606 |
. . . . . . 7
|
70 | 48, 49, 50, 34, 32, 33, 35, 67, 68, 69 | syl333anc 1358 |
. . . . . 6
|
71 | 9, 11, 59 | llni2 34798 |
. . . . . 6
|
72 | 1, 63, 66, 70, 71 | syl31anc 1329 |
. . . . 5
|
73 | | eqid 2622 |
. . . . . 6
|
74 | 9, 10, 11, 59, 73 | 2llnmj 34846 |
. . . . 5
|
75 | 1, 61, 72, 74 | syl3anc 1326 |
. . . 4
|
76 | 47, 75 | mpbid 222 |
. . 3
|
77 | 30, 76 | eqeltrd 2701 |
. 2
|
78 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20l1 35608 |
. . . 4
|
79 | 48, 49, 50, 18, 7, 43, 51, 36, 39, 78 | syl333anc 1358 |
. . 3
|
80 | | eqid 2622 |
. . . . 5
|
81 | 8, 9, 10, 11, 12, 13, 23, 14, 26, 19, 80 | cdleme20l1 35608 |
. . . 4
|
82 | 48, 49, 50, 18, 22, 64, 51, 37, 39, 81 | syl333anc 1358 |
. . 3
|
83 | 9, 10, 11, 59, 73 | 2llnmj 34846 |
. . 3
|
84 | 1, 79, 82, 83 | syl3anc 1326 |
. 2
|
85 | 77, 84 | mpbird 247 |
1
|