Proof of Theorem cdlemeg46req
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. 2
|
2 | | simp12l 1174 |
. . 3
|
3 | | simp13l 1176 |
. . 3
|
4 | | simp21 1094 |
. . 3
|
5 | | cdlemef46g.j |
. . . 4
|
6 | | cdlemef46g.a |
. . . 4
|
7 | | eqid 2622 |
. . . 4
|
8 | 5, 6, 7 | llni2 34798 |
. . 3
|
9 | 1, 2, 3, 4, 8 | syl31anc 1329 |
. 2
|
10 | | simp1 1061 |
. . . . 5
|
11 | | simp23 1096 |
. . . . 5
|
12 | | cdlemef46g.b |
. . . . . 6
|
13 | | cdlemef46g.l |
. . . . . 6
|
14 | | cdlemef46g.m |
. . . . . 6
|
15 | | cdlemef46g.h |
. . . . . 6
|
16 | | cdlemef46g.u |
. . . . . 6
|
17 | | cdlemef46g.d |
. . . . . 6
|
18 | | cdlemefs46g.e |
. . . . . 6
|
19 | | cdlemef46g.f |
. . . . . 6
|
20 | | cdlemef46.v |
. . . . . 6
|
21 | | cdlemef46.n |
. . . . . 6
|
22 | | cdlemefs46.o |
. . . . . 6
|
23 | | cdlemef46.g |
. . . . . 6
|
24 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemeg46fvaw 35804 |
. . . . 5
|
25 | 10, 11, 4, 24 | syl3anc 1326 |
. . . 4
|
26 | 25 | simpld 475 |
. . 3
|
27 | | simp11 1091 |
. . . 4
|
28 | | simp22 1095 |
. . . . 5
|
29 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19 | cdleme46fvaw 35789 |
. . . . 5
|
30 | 10, 28, 29 | syl2anc 693 |
. . . 4
|
31 | | simp23l 1182 |
. . . 4
|
32 | | simp3l 1089 |
. . . . . 6
|
33 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19 | cdleme46fsvlpq 35793 |
. . . . . 6
|
34 | 10, 4, 28, 32, 33 | syl121anc 1331 |
. . . . 5
|
35 | | simp3r 1090 |
. . . . 5
|
36 | | nbrne2 4673 |
. . . . 5
|
37 | 34, 35, 36 | syl2anc 693 |
. . . 4
|
38 | | cdlemeg46.x |
. . . . 5
|
39 | 13, 5, 14, 6, 15, 38 | lhpat2 35331 |
. . . 4
|
40 | 27, 30, 31, 37, 39 | syl112anc 1330 |
. . 3
|
41 | | hllat 34650 |
. . . . . . . 8
|
42 | 1, 41 | syl 17 |
. . . . . . 7
|
43 | 30 | simpld 475 |
. . . . . . . 8
|
44 | 12, 5, 6 | hlatjcl 34653 |
. . . . . . . 8
|
45 | 1, 43, 31, 44 | syl3anc 1326 |
. . . . . . 7
|
46 | | simp11r 1173 |
. . . . . . . 8
|
47 | 12, 15 | lhpbase 35284 |
. . . . . . . 8
|
48 | 46, 47 | syl 17 |
. . . . . . 7
|
49 | 12, 13, 14 | latmle2 17077 |
. . . . . . 7
|
50 | 42, 45, 48, 49 | syl3anc 1326 |
. . . . . 6
|
51 | 38, 50 | syl5eqbr 4688 |
. . . . 5
|
52 | 25 | simprd 479 |
. . . . 5
|
53 | | nbrne2 4673 |
. . . . 5
|
54 | 51, 52, 53 | syl2anc 693 |
. . . 4
|
55 | 54 | necomd 2849 |
. . 3
|
56 | 5, 6, 7 | llni2 34798 |
. . 3
|
57 | 1, 26, 40, 55, 56 | syl31anc 1329 |
. 2
|
58 | | simp22l 1180 |
. 2
|
59 | 13, 5, 6 | hlatlej1 34661 |
. . . . 5
|
60 | 1, 26, 40, 59 | syl3anc 1326 |
. . . 4
|
61 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemeg46nlpq 35805 |
. . . . 5
|
62 | 10, 4, 11, 35, 61 | syl121anc 1331 |
. . . 4
|
63 | | nbrne1 4672 |
. . . 4
|
64 | 60, 62, 63 | syl2anc 693 |
. . 3
|
65 | 64 | necomd 2849 |
. 2
|
66 | | cdlemeg46.y |
. . . 4
|
67 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38 | cdlemeg46rgv 35816 |
. . 3
|
68 | 12, 6 | atbase 34576 |
. . . . 5
|
69 | 58, 68 | syl 17 |
. . . 4
|
70 | 12, 5, 6 | hlatjcl 34653 |
. . . . 5
|
71 | 1, 2, 3, 70 | syl3anc 1326 |
. . . 4
|
72 | 12, 5, 6 | hlatjcl 34653 |
. . . . 5
|
73 | 1, 26, 40, 72 | syl3anc 1326 |
. . . 4
|
74 | 12, 13, 14 | latlem12 17078 |
. . . 4
|
75 | 42, 69, 71, 73, 74 | syl13anc 1328 |
. . 3
|
76 | 32, 67, 75 | mpbi2and 956 |
. 2
|
77 | 13, 14, 6, 7 | 2llnmeqat 34857 |
. 2
|
78 | 1, 9, 57, 58, 65, 76, 77 | syl132anc 1344 |
1
|