Proof of Theorem cdleme20l2
Step | Hyp | Ref
| Expression |
1 | | simp11l 1068 |
. . . . 5
     
       
     
 
       
         |
2 | | hllat 29850 |
. . . . 5
   |
3 | 1, 2 | syl 16 |
. . . 4
     
       
     
 
       
         |
4 | | simp11r 1069 |
. . . . 5
     
       
     
 
       
         |
5 | | simp12l 1070 |
. . . . 5
     
       
     
 
       
         |
6 | | simp13l 1072 |
. . . . 5
     
       
     
 
       
         |
7 | | simp22l 1076 |
. . . . 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 2408 |
. . . . . 6
         |
16 | 8, 9, 10, 11, 12, 13, 14, 15 | cdleme1b 30712 |
. . . . 5
      
      |
17 | 1, 4, 5, 6, 7, 16 | syl23anc 1191 |
. . . 4
     
       
     
 
       
             |
18 | | simp21l 1074 |
. . . . 5
     
       
     
 
       
         |
19 | | cdleme19.d |
. . . . . 6
  
  |
20 | 8, 9, 10, 11, 12, 19, 15 | cdlemedb 30783 |
. . . . 5
      
      |
21 | 1, 4, 18, 7, 20 | syl22anc 1185 |
. . . 4
     
       
     
 
       
             |
22 | | simp23l 1078 |
. . . . 5
     
       
     
 
       
         |
23 | | cdleme19.g |
. . . . . 6
  
   
    |
24 | 8, 9, 10, 11, 12, 13, 23, 15 | cdleme1b 30712 |
. . . . 5
      
      |
25 | 1, 4, 5, 6, 22, 24 | syl23anc 1191 |
. . . 4
     
       
     
 
       
             |
26 | | cdleme19.y |
. . . . . 6
  
  |
27 | 8, 9, 10, 11, 12, 26, 15 | cdlemedb 30783 |
. . . . 5
      
      |
28 | 1, 4, 18, 22, 27 | syl22anc 1185 |
. . . 4
     
       
     
 
       
             |
29 | 15, 9 | latj4 14489 |
. . . 4
  
   
     
   
         
          |
30 | 3, 17, 21, 25, 28, 29 | syl122anc 1193 |
. . 3
     
       
     
 
       
          
          |
31 | | simp1 957 |
. . . . . 6
     
       
     
 
       
          
      |
32 | | simp22 991 |
. . . . . 6
     
       
     
 
       
           |
33 | | simp23 992 |
. . . . . 6
     
       
     
 
       
           |
34 | | simp21 990 |
. . . . . 6
     
       
     
 
       
           |
35 | | simp31 993 |
. . . . . 6
     
       
     
 
       
       
   |
36 | | simp321 1107 |
. . . . . . 7
     
       
     
 
       
      
    |
37 | | simp322 1108 |
. . . . . . 7
     
       
     
 
       
      
    |
38 | 36, 37 | jca 519 |
. . . . . 6
     
       
     
 
       
         
     |
39 | | simp323 1109 |
. . . . . 6
     
       
     
 
       
           |
40 | | cdleme20.v |
. . . . . . 7
  
  |
41 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20d 30798 |
. . . . . 6
     
       
     
 
           
     |
42 | 31, 32, 33, 34, 35, 38, 39, 41 | syl133anc 1207 |
. . . . 5
     
       
     
 
       
          
    |
43 | | simp22r 1077 |
. . . . . 6
     
       
     
 
       
      
  |
44 | | simp31r 1081 |
. . . . . 6
     
       
     
 
       
         |
45 | 8, 9, 10, 11, 12, 40 | lhpat2 30531 |
. . . . . 6
      
    |
46 | 1, 4, 7, 43, 22, 44, 45 | syl222anc 1200 |
. . . . 5
     
       
     
 
       
         |
47 | 42, 46 | eqeltrd 2482 |
. . . 4
     
       
     
 
       
          
    |
48 | | simp11 987 |
. . . . . . 7
     
       
     
 
       
           |
49 | | simp12 988 |
. . . . . . 7
     
       
     
 
       
           |
50 | | simp13 989 |
. . . . . . 7
     
       
     
 
       
           |
51 | | simp31l 1080 |
. . . . . . 7
     
       
     
 
       
         |
52 | 8, 9, 10, 11, 12, 13, 14 | cdleme3fa 30722 |
. . . . . . 7
       
    
   
  |
53 | 48, 49, 50, 32, 51, 36, 52 | syl132anc 1202 |
. . . . . 6
     
       
     
 
       
         |
54 | 8, 9, 10, 11, 12, 13, 23 | cdleme3fa 30722 |
. . . . . . 7
       
    
   
  |
55 | 48, 49, 50, 33, 51, 37, 54 | syl132anc 1202 |
. . . . . 6
     
       
     
 
       
         |
56 | | simp33r 1085 |
. . . . . . 7
     
       
     
 
       
      
    |
57 | 8, 9, 10, 11, 12, 13, 14, 23 | cdleme16b 30765 |
. . . . . . 7
     
       
 
  
 
 
   
  |
58 | 31, 32, 33, 35, 36, 37, 56, 57 | syl133anc 1207 |
. . . . . 6
     
       
     
 
       
         |
59 | | eqid 2408 |
. . . . . . 7
         |
60 | 9, 11, 59 | llni2 29998 |
. . . . . 6
  


        |
61 | 1, 53, 55, 58, 60 | syl31anc 1187 |
. . . . 5
     
       
     
 
       
               |
62 | 8, 9, 10, 11, 12, 19 | cdlemeda 30784 |
. . . . . . 7
      
     
  |
63 | 1, 4, 7, 43, 18, 39, 36, 62 | syl223anc 1210 |
. . . . . 6
     
       
     
 
       
         |
64 | | simp23r 1079 |
. . . . . . 7
     
       
     
 
       
      
  |
65 | 8, 9, 10, 11, 12, 26 | cdlemeda 30784 |
. . . . . . 7
      
     
  |
66 | 1, 4, 22, 64, 18, 39, 37, 65 | syl223anc 1210 |
. . . . . 6
     
       
     
 
       
         |
67 | | simp32 994 |
. . . . . . 7
     
       
     
 
       
         
 
     |
68 | | simp33l 1084 |
. . . . . . 7
     
       
     
 
       
      
    |
69 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20j 30804 |
. . . . . . 7
     
       
     
 
             |
70 | 48, 49, 50, 34, 32, 33, 35, 67, 68, 69 | syl333anc 1216 |
. . . . . 6
     
       
     
 
       
         |
71 | 9, 11, 59 | llni2 29998 |
. . . . . 6
  


        |
72 | 1, 63, 66, 70, 71 | syl31anc 1187 |
. . . . 5
     
       
     
 
       
               |
73 | | eqid 2408 |
. . . . . 6
         |
74 | 9, 10, 11, 59, 73 | 2llnmj 30046 |
. . . . 5
  
    
                
          |
75 | 1, 61, 72, 74 | syl3anc 1184 |
. . . 4
     
       
     
 
       
                
          |
76 | 47, 75 | mpbid 202 |
. . 3
     
       
     
 
       
          
        |
77 | 30, 76 | eqeltrd 2482 |
. 2
     
       
     
 
       
          
        |
78 | 8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40 | cdleme20l1 30806 |
. . . 4
     
    
 
 
            |
79 | 48, 49, 50, 18, 7, 43, 51, 36, 39, 78 | syl333anc 1216 |
. . 3
     
       
     
 
       
               |
80 | | eqid 2408 |
. . . . 5
      
  |
81 | 8, 9, 10, 11, 12, 13, 23, 14, 26, 19, 80 | cdleme20l1 30806 |
. . . 4
     
    
 
 
            |
82 | 48, 49, 50, 18, 22, 64, 51, 37, 39, 81 | syl333anc 1216 |
. . 3
     
       
     
 
       
               |
83 | 9, 10, 11, 59, 73 | 2llnmj 30046 |
. . 3
  
    
                
          |
84 | 1, 79, 82, 83 | syl3anc 1184 |
. 2
     
       
     
 
       
                
          |
85 | 77, 84 | mpbird 224 |
1
     
       
     
 
       
          
    |