Proof of Theorem cdlemg33a
Step | Hyp | Ref
| Expression |
1 | | simp11 1018 |
. . 3
     
       
 
   

                 |
2 | | simp12 1019 |
. . 3
     
       
 
   

                 |
3 | | simp13 1020 |
. . 3
     
       
 
   

                 |
4 | | simp22l 1107 |
. . . 4
     
       
 
   

               |
5 | | simp21 1021 |
. . . . 5
     
       
 
   

                 |
6 | | simp23l 1109 |
. . . . 5
     
       
 
   

               |
7 | | simp32 1025 |
. . . . 5
     
       
 
   

                   |
8 | | cdlemg12.l |
. . . . . 6
     |
9 | | cdlemg12.j |
. . . . . 6
     |
10 | | cdlemg12.m |
. . . . . 6
     |
11 | | cdlemg12.a |
. . . . . 6
     |
12 | | cdlemg12.h |
. . . . . 6
     |
13 | | cdlemg12.t |
. . . . . 6
         |
14 | | cdlemg12b.r |
. . . . . 6
         |
15 | | cdlemg31.n |
. . . . . 6
           |
16 | 8, 9, 10, 11, 12, 13, 14, 15 | cdlemg31d 34650 |
. . . . 5
       
    
   
    |
17 | 1, 2, 3, 5, 6, 7, 4, 16 | syl133anc 1242 |
. . . 4
     
       
 
   

            
  |
18 | 4, 17 | jca 532 |
. . 3
     
       
 
   

                 |
19 | | simp31l 1111 |
. . 3
     
       
 
   

               |
20 | | simp22r 1108 |
. . . 4
     
       
 
   

               |
21 | | simp31r 1112 |
. . . 4
     
       
 
   

               |
22 | 20, 21 | jca 532 |
. . 3
     
       
 
   

                 |
23 | | simp33 1026 |
. . 3
     
       
 
   

              
       |
24 | 8, 9, 11, 12 | 4atex3 34031 |
. . 3
       
    



         

      |
25 | 1, 2, 3, 18, 19, 22, 23, 24 | syl133anc 1242 |
. 2
     
       
 
   

              

      |
26 | | idd 24 |
. . . . 5
      
       
 
   

             

   |
27 | | idd 24 |
. . . . 5
      
       
 
   

             

   |
28 | | simp12l 1101 |
. . . . . . . . . 10
     
       
 
   

               |
29 | | simp13l 1103 |
. . . . . . . . . 10
     
       
 
   

               |
30 | | simp21l 1105 |
. . . . . . . . . 10
     
       
 
   

               |
31 | 8, 9, 10, 11, 12, 13, 14, 15 | cdlemg31a 34647 |
. . . . . . . . . 10
      
 
    |
32 | 1, 28, 29, 30, 6, 31 | syl122anc 1228 |
. . . . . . . . 9
     
       
 
   

                 |
33 | | simp23r 1110 |
. . . . . . . . . 10
     
       
 
   

               |
34 | | cdlemg33.o |
. . . . . . . . . . 11
           |
35 | 8, 9, 10, 11, 12, 13, 14, 34 | cdlemg31a 34647 |
. . . . . . . . . 10
      
 
    |
36 | 1, 28, 29, 30, 33, 35 | syl122anc 1228 |
. . . . . . . . 9
     
       
 
   

                 |
37 | | simp11l 1099 |
. . . . . . . . . . 11
     
       
 
   

               |
38 | | hllat 33314 |
. . . . . . . . . . 11
   |
39 | 37, 38 | syl 16 |
. . . . . . . . . 10
     
       
 
   

               |
40 | | eqid 2451 |
. . . . . . . . . . . 12
         |
41 | 40, 11 | atbase 33240 |
. . . . . . . . . . 11
       |
42 | 4, 41 | syl 16 |
. . . . . . . . . 10
     
       
 
   

                   |
43 | 40, 9, 11 | hlatjcl 33317 |
. . . . . . . . . . 11
 
         |
44 | 37, 28, 30, 43 | syl3anc 1219 |
. . . . . . . . . 10
     
       
 
   

                     |
45 | 40, 11 | atbase 33240 |
. . . . . . . . . . 11
       |
46 | 20, 45 | syl 16 |
. . . . . . . . . 10
     
       
 
   

                   |
47 | 40, 8, 9 | latjlej12 15339 |
. . . . . . . . . 10
  
    
      
                    
   
     |
48 | 39, 42, 44, 46, 44, 47 | syl122anc 1228 |
. . . . . . . . 9
     
       
 
   

                
  
           |
49 | 32, 36, 48 | mp2and 679 |
. . . . . . . 8
     
       
 
   

              
   
    |
50 | 40, 9 | latjidm 15346 |
. . . . . . . . 9
  
        
       |
51 | 39, 44, 50 | syl2anc 661 |
. . . . . . . 8
     
       
 
   

                
      |
52 | 49, 51 | breqtrd 4414 |
. . . . . . 7
     
       
 
   

              
    |
53 | 52 | adantr 465 |
. . . . . 6
      
       
 
   

             
      |
54 | 39 | adantr 465 |
. . . . . . 7
      
       
 
   

             
  |
55 | 40, 11 | atbase 33240 |
. . . . . . . 8
       |
56 | 55 | adantl 466 |
. . . . . . 7
      
       
 
   

             
      |
57 | 40, 9, 11 | hlatjcl 33317 |
. . . . . . . . 9
 
         |
58 | 37, 4, 20, 57 | syl3anc 1219 |
. . . . . . . 8
     
       
 
   

                     |
59 | 58 | adantr 465 |
. . . . . . 7
      
       
 
   

             
        |
60 | 44 | adantr 465 |
. . . . . . 7
      
       
 
   

             
        |
61 | 40, 8 | lattr 15328 |
. . . . . . 7
                       
  
        |
62 | 54, 56, 59, 60, 61 | syl13anc 1221 |
. . . . . 6
      
       
 
   

             
      
 
     |
63 | 53, 62 | mpan2d 674 |
. . . . 5
      
       
 
   

             
  
     |
64 | 26, 27, 63 | 3anim123d 1297 |
. . . 4
      
       
 
   

             
            |
65 | 64 | anim2d 565 |
. . 3
      
       
 
   

             
 

   
         |
66 | 65 | reximdva 2924 |
. 2
     
       
 
   

              
      


       |
67 | 25, 66 | mpd 15 |
1
     
       
 
   

              

      |