Step | Hyp | Ref
| Expression |
1 | | 3dim0.j |
. . . 4
     |
2 | | 3dim0.l |
. . . 4
     |
3 | | 3dim0.a |
. . . 4
     |
4 | 1, 2, 3 | 3dim0 33016 |
. . 3
 



  
       |
5 | 4 | adantr 467 |
. 2
 
  


  
       |
6 | | simpl2 1011 |
. . . . . . . . . . 11
     
   
       
   |
7 | 1, 2, 3 | 3dimlem1 33017 |
. . . . . . . . . . . 12
    
     
  
       |
8 | 7 | 3ad2antl3 1171 |
. . . . . . . . . . 11
     
   
                 |
9 | 1, 2, 3 | 3dim1lem5 33025 |
. . . . . . . . . . 11
  

  
      



 
       |
10 | 6, 8, 9 | syl2anc 666 |
. . . . . . . . . 10
     
   
       



 
       |
11 | | simp13 1039 |
. . . . . . . . . . . . . 14
  
 

  
        |
12 | | simp22 1041 |
. . . . . . . . . . . . . 14
  
 

  
        |
13 | | simp23 1042 |
. . . . . . . . . . . . . 14
  
 

  
     
  |
14 | 11, 12, 13 | 3jca 1187 |
. . . . . . . . . . . . 13
  
 

  
      
   |
15 | 14 | ad2antrr 731 |
. . . . . . . . . . . 12
    
 
   
          
   |
16 | | simpll1 1046 |
. . . . . . . . . . . . 13
    
 
   
          
   |
17 | | simp21 1040 |
. . . . . . . . . . . . . . 15
  
 

  
     
  |
18 | | simp32 1044 |
. . . . . . . . . . . . . . 15
  
 

  
     
    |
19 | | simp33 1045 |
. . . . . . . . . . . . . . 15
  
 

  
     
      |
20 | 17, 18, 19 | 3jca 1187 |
. . . . . . . . . . . . . 14
  
 

  
        
       |
21 | 20 | ad2antrr 731 |
. . . . . . . . . . . . 13
    
 
   
          
 
       |
22 | | simplr 761 |
. . . . . . . . . . . . 13
    
 
   
            |
23 | | simpr 463 |
. . . . . . . . . . . . 13
    
 
   
              |
24 | 1, 2, 3 | 3dimlem2 33018 |
. . . . . . . . . . . . 13
  
   
                    |
25 | 16, 21, 22, 23, 24 | syl112anc 1271 |
. . . . . . . . . . . 12
    
 
   
                    |
26 | 1, 2, 3 | 3dim1lem5 33025 |
. . . . . . . . . . . 12
  


 
      



 
       |
27 | 15, 25, 26 | syl2anc 666 |
. . . . . . . . . . 11
    
 
   
          



 
       |
28 | 11, 17, 13 | 3jca 1187 |
. . . . . . . . . . . . . . 15
  
 

  
      
   |
29 | 28 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    
 
   
                    |
30 | | simp1 1007 |
. . . . . . . . . . . . . . . . 17
  
 

  
      
   |
31 | 17, 12 | jca 535 |
. . . . . . . . . . . . . . . . 17
  
 

  
      
   |
32 | | simp31 1043 |
. . . . . . . . . . . . . . . . . 18
  
 

  
        |
33 | 32, 19 | jca 535 |
. . . . . . . . . . . . . . . . 17
  
 

  
              |
34 | 30, 31, 33 | 3jca 1187 |
. . . . . . . . . . . . . . . 16
  
 

  
         
          |
35 | 34 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
    
 
   
                 
 
          |
36 | | simplrl 769 |
. . . . . . . . . . . . . . 15
    
 
   
                  |
37 | | simplrr 770 |
. . . . . . . . . . . . . . 15
    
 
   
               
    |
38 | | simpr 463 |
. . . . . . . . . . . . . . 15
    
 
   
                      |
39 | 1, 2, 3 | 3dimlem3 33020 |
. . . . . . . . . . . . . . 15
     
                   
       |
40 | 35, 36, 37, 38, 39 | syl13anc 1269 |
. . . . . . . . . . . . . 14
    
 
   
                  
       |
41 | 1, 2, 3 | 3dim1lem5 33025 |
. . . . . . . . . . . . . 14
  


 
      



 
       |
42 | 29, 40, 41 | syl2anc 666 |
. . . . . . . . . . . . 13
    
 
   
                 


 
       |
43 | 11, 17, 12 | 3jca 1187 |
. . . . . . . . . . . . . . 15
  
 

  
      
   |
44 | 43 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    
 
   
             
 

   |
45 | | simpl1 1010 |
. . . . . . . . . . . . . . . . 17
     
   
               |
46 | | simpl21 1085 |
. . . . . . . . . . . . . . . . . 18
     
   
             |
47 | | simpl22 1086 |
. . . . . . . . . . . . . . . . . 18
     
   
             |
48 | 46, 47 | jca 535 |
. . . . . . . . . . . . . . . . 17
     
   
               |
49 | | simpl31 1088 |
. . . . . . . . . . . . . . . . . 18
     
   
             |
50 | | simpl32 1089 |
. . . . . . . . . . . . . . . . . 18
     
   
          
    |
51 | 49, 50 | jca 535 |
. . . . . . . . . . . . . . . . 17
     
   
                 |
52 | 45, 48, 51 | 3jca 1187 |
. . . . . . . . . . . . . . . 16
     
   
            
 
        |
53 | 52 | adantr 467 |
. . . . . . . . . . . . . . 15
    
 
   
             
 
 
 
        |
54 | | simplr 761 |
. . . . . . . . . . . . . . 15
    
 
   
             
 

     |
55 | | simpr 463 |
. . . . . . . . . . . . . . 15
    
 
   
             
 
      |
56 | 1, 2, 3 | 3dimlem4 33023 |
. . . . . . . . . . . . . . 15
     
         
       
       |
57 | 53, 54, 55, 56 | syl3anc 1267 |
. . . . . . . . . . . . . 14
    
 
   
             
 

 
       |
58 | 1, 2, 3 | 3dim1lem5 33025 |
. . . . . . . . . . . . . 14
  


 
      



 
       |
59 | 44, 57, 58 | syl2anc 666 |
. . . . . . . . . . . . 13
    
 
   
             
 




 
       |
60 | 42, 59 | pm2.61dan 799 |
. . . . . . . . . . . 12
     
   
            


 
       |
61 | 60 | anassrs 653 |
. . . . . . . . . . 11
    
 
   
          



 
       |
62 | 27, 61 | pm2.61dan 799 |
. . . . . . . . . 10
     
   
       



 
       |
63 | 10, 62 | pm2.61dane 2710 |
. . . . . . . . 9
  
 

  
      



 
       |
64 | 63 | 3exp 1206 |
. . . . . . . 8
 
       
      


 
         |
65 | 64 | 3expd 1225 |
. . . . . . 7
 
       
     



 
           |
66 | 65 | 3exp 1206 |
. . . . . 6
 
       
     



 
             |
67 | 66 | imp43 599 |
. . . . 5
            
     



 
          |
68 | 67 | impd 433 |
. . . 4
             
      


 
         |
69 | 68 | rexlimdvv 2884 |
. . 3
            
     



 
        |
70 | 69 | rexlimdvva 2885 |
. 2
 
        
     



 
        |
71 | 5, 70 | mpd 15 |
1
 
  


 
       |