Step | Hyp | Ref
| Expression |
1 | | eqid 2454 |
. . 3
         |
2 | | eqid 2454 |
. . 3
         |
3 | | eqid 2454 |
. . 3
         |
4 | | eqid 2454 |
. . 3
         |
5 | 1, 2, 3, 4 | hlhgt4 33371 |
. 2
                                                           |
6 | | simpl1 991 |
. . . . . . . . 9
       
         
                                         |
7 | | hlop 33346 |
. . . . . . . . . 10
   |
8 | 1, 3 | op0cl 33168 |
. . . . . . . . . 10
           |
9 | 6, 7, 8 | 3syl 20 |
. . . . . . . . 9
       
         
                                                 |
10 | | simpl2l 1041 |
. . . . . . . . 9
       
         
                                             |
11 | | simprll 761 |
. . . . . . . . 9
       
         
                                                   |
12 | | eqid 2454 |
. . . . . . . . . 10
         |
13 | | athgt.j |
. . . . . . . . . 10
     |
14 | | athgt.c |
. . . . . . . . . 10
   |
15 | | athgt.a |
. . . . . . . . . 10
     |
16 | 1, 12, 2, 13, 14, 15 | hlrelat3 33395 |
. . . . . . . . 9
                           
            
               |
17 | 6, 9, 10, 11, 16 | syl31anc 1222 |
. . . . . . . 8
       
         
                                                   
                |
18 | | simp11 1018 |
. . . . . . . . . . . . . 14
       
         
                                     
   |
19 | | simp3 990 |
. . . . . . . . . . . . . 14
       
         
                                     
   |
20 | 3, 14, 15 | atcvr0 33272 |
. . . . . . . . . . . . . 14
 
         |
21 | 18, 19, 20 | syl2anc 661 |
. . . . . . . . . . . . 13
       
         
                                     
         |
22 | | hlol 33345 |
. . . . . . . . . . . . . . 15
   |
23 | 18, 22 | syl 16 |
. . . . . . . . . . . . . 14
       
         
                                     
   |
24 | 1, 15 | atbase 33273 |
. . . . . . . . . . . . . . 15
       |
25 | 24 | 3ad2ant3 1011 |
. . . . . . . . . . . . . 14
       
         
                                     
       |
26 | 1, 13, 3 | olj02 33210 |
. . . . . . . . . . . . . 14
 
             |
27 | 23, 25, 26 | syl2anc 661 |
. . . . . . . . . . . . 13
       
         
                                     
         |
28 | 21, 27 | breqtrrd 4427 |
. . . . . . . . . . . 12
       
         
                                     
               |
29 | 28 | biantrurd 508 |
. . . . . . . . . . 11
       
         
                                     
                         
                 |
30 | 27 | breq1d 4411 |
. . . . . . . . . . 11
       
         
                                     
                       |
31 | 29, 30 | bitr3d 255 |
. . . . . . . . . 10
       
         
                                     
              
                      |
32 | 31 | 3expa 1188 |
. . . . . . . . 9
        
    
    
                                       
                                    |
33 | 32 | rexbidva 2865 |
. . . . . . . 8
       
         
                                        
            
                       |
34 | 17, 33 | mpbid 210 |
. . . . . . 7
       
         
                                                |
35 | | simp11 1018 |
. . . . . . . . . . . 12
       
         
                                      
       
  |
36 | 25 | 3adant3r 1216 |
. . . . . . . . . . . 12
       
         
                                      
       
      |
37 | | simp12r 1102 |
. . . . . . . . . . . 12
       
         
                                      
       
      |
38 | | simp3r 1017 |
. . . . . . . . . . . . 13
       
         
                                      
       
        |
39 | | simp2lr 1056 |
. . . . . . . . . . . . 13
       
         
                                      
       
        |
40 | | hlpos 33349 |
. . . . . . . . . . . . . . 15
   |
41 | 35, 40 | syl 16 |
. . . . . . . . . . . . . 14
       
         
                                      
       
  |
42 | | simp12l 1101 |
. . . . . . . . . . . . . 14
       
         
                                      
       
      |
43 | 1, 12, 2 | plelttr 15262 |
. . . . . . . . . . . . . 14
          
                    
         |
44 | 41, 36, 42, 37, 43 | syl13anc 1221 |
. . . . . . . . . . . . 13
       
         
                                      
       
                        |
45 | 38, 39, 44 | mp2and 679 |
. . . . . . . . . . . 12
       
         
                                      
       
        |
46 | 1, 12, 2, 13, 14, 15 | hlrelat3 33395 |
. . . . . . . . . . . 12
                   
                |
47 | 35, 36, 37, 45, 46 | syl31anc 1222 |
. . . . . . . . . . 11
       
         
                                      
       

     
          |
48 | | simp11 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 
           |
49 | | hllat 33347 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
50 | 48, 49 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
           |
51 | | simp3ll 1059 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
           |
52 | 51, 24 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
               |
53 | | simp3lr 1060 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
           |
54 | 1, 15 | atbase 33273 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
55 | 53, 54 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
               |
56 | 1, 13 | latjcl 15341 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         
       |
57 | 50, 52, 55, 56 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 
                 |
58 | | simp13 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 
               |
59 | | simp3r 1017 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                   |
60 | | simp2l 1014 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                 |
61 | 48, 40 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
           |
62 | | simp12 1019 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
               |
63 | 1, 12, 2 | plelttr 15262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
                      
           |
64 | 61, 57, 62, 58, 63 | syl13anc 1221 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                                     |
65 | 59, 60, 64 | mp2and 679 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 
                   |
66 | 1, 12, 2, 13, 14, 15 | hlrelat3 33395 |
. . . . . . . . . . . . . . . . . . . . . 22
              
        
       
              |
67 | 48, 57, 58, 65, 66 | syl31anc 1222 |
. . . . . . . . . . . . . . . . . . . . 21
                                 
                 
              |
68 | | simp1ll 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       
                    
  |
69 | 68, 49 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
  |
70 | | simp2ll 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                       
                    
  |
71 | 70, 24 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                    
      |
72 | | simp2lr 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                       
                    
  |
73 | 72, 54 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                    
      |
74 | 69, 71, 73, 56 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
        |
75 | | simp3l 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                    
  |
76 | 1, 15 | atbase 33273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
77 | 75, 76 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
      |
78 | 1, 13 | latjcl 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
    
    
 
        |
79 | 69, 74, 77, 78 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       
                    
 
        |
80 | 1, 4 | op1cl 33169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
81 | 68, 7, 80 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       
                    
          |
82 | | simp3r 1017 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
 
          |
83 | | simp1r 1013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
            |
84 | 68, 40 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                    
  |
85 | | simp1lr 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       
                    
      |
86 | 1, 12, 2 | plelttr 15262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
                                
 
               |
87 | 84, 79, 85, 81, 86 | syl13anc 1221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       
                    
                                        |
88 | 82, 83, 87 | mp2and 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       
                    
 
              |
89 | 1, 12, 2, 13, 14, 15 | hlrelat3 33395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                      
            
           
                    |
90 | 68, 79, 81, 88, 89 | syl31anc 1222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                       
                    

   
             
              |
91 | | simpl 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
      
                     
    |
92 | 91 | reximi 2929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
      
            
         
    |
93 | 90, 92 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                       
                    

 
        
   |
94 | 93 | 3exp 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     
              
        
         
      |
95 | 94 | exp4a 606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                     
          
   
       
 
        
      |
96 | 95 | ex 434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                  
          
   
       
 
        
       |
97 | 96 | 3adant2 1007 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                        
                              
        |
98 | 97 | 3imp 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       

                                
      |
99 | 98 | 3adant2l 1213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
         
   
       
 
        
     |
100 | 99 | imp 429 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
    
                     
         
   
       
 
        
    |
101 | 100 | anim2d 565 |
. . . . . . . . . . . . . . . . . . . . . 22
       
    
                     
         
                             

 
        
     |
102 | 101 | reximdva 2934 |
. . . . . . . . . . . . . . . . . . . . 21
                                 
          
 
         
        
       
           
      |
103 | 67, 102 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
                                 
                 
           
     |
104 | 103 | 3exp 1187 |
. . . . . . . . . . . . . . . . . . 19
 
                           
  

        

 
       
  
              |
105 | 104 | exp4a 606 |
. . . . . . . . . . . . . . . . . 18
 
                           
 
                  
           
        |
106 | 105 | exp4a 606 |
. . . . . . . . . . . . . . . . 17
 
                           

          
       
           
         |
107 | 106 | 3adant2l 1213 |
. . . . . . . . . . . . . . . 16
  
   
    
                                           
           
         |
108 | 107 | 3imp1 1201 |
. . . . . . . . . . . . . . 15
        
    
    
                 


 
       
 
       
  
             |
109 | 108 | anim2d 565 |
. . . . . . . . . . . . . 14
        
    
    
                 


      
                      

 
        
      |
110 | 109 | reximdva 2934 |
. . . . . . . . . . . . 13
       
         
                 
       
        

     
            
              |
111 | 110 | 3adant2l 1213 |
. . . . . . . . . . . 12
       
         
                                     
       
        

     
            
              |
112 | 111 | 3adant3r 1216 |
. . . . . . . . . . 11
       
         
                                      
       
 
     
        
              

 
        
      |
113 | 47, 112 | mpd 15 |
. . . . . . . . . 10
       
         
                                      
       

     
            
             |
114 | 113 | 3expia 1190 |
. . . . . . . . 9
       
         
                                                
              

 
        
      |
115 | 114 | expd 436 |
. . . . . . . 8
       
         
                                       
       
     
            
               |
116 | 115 | reximdvai 2932 |
. . . . . . 7
       
         
                                        
       
              

 
        
      |
117 | 34, 116 | mpd 15 |
. . . . . 6
       
         
                                        
              

 
        
     |
118 | 117 | 3exp1 1204 |
. . . . 5
      
         
                                        
              

 
        
        |
119 | 118 | imp 429 |
. . . 4
  
   
          
                                        
              

 
        
       |
120 | 119 | rexlimdv 2946 |
. . 3
  
   
                                                   

     
            
              |
121 | 120 | rexlimdvva 2954 |
. 2
  
                                                       

     
            
              |
122 | 5, 121 | mpd 15 |
1
 

     
            
             |