Step | Hyp | Ref
| Expression |
1 | | simprrl 741 |
. . . . . . . . 9
        
             
             
                Cgr      Cgr 
    
    Cgr 
         |
2 | | simprlr 740 |
. . . . . . . . 9
        
             
             
                Cgr      Cgr 
    
    Cgr 
       Cgr     |
3 | | simpl11 1032 |
. . . . . . . . . . 11
       
             
             
             |
4 | | simpl21 1035 |
. . . . . . . . . . 11
       
             
             
                 |
5 | | simpr 448 |
. . . . . . . . . . 11
       
             
             
                 |
6 | | simpl22 1036 |
. . . . . . . . . . 11
       
             
             
                 |
7 | | simpl32 1039 |
. . . . . . . . . . 11
       
             
             
                 |
8 | | simpl33 1040 |
. . . . . . . . . . 11
       
             
             
                 |
9 | | cgrxfr 25897 |
. . . . . . . . . . 11
  
   
         
             
    Cgr 
           
      Cgr3 
        |
10 | 3, 4, 5, 6, 7, 8, 9 | syl132anc 1202 |
. . . . . . . . . 10
       
             
             
               
   Cgr   
        
       Cgr3          |
11 | 10 | adantr 452 |
. . . . . . . . 9
        
             
             
                Cgr      Cgr 
    
    Cgr 
        
   Cgr   
        
       Cgr3          |
12 | 1, 2, 11 | mp2and 661 |
. . . . . . . 8
        
             
             
                Cgr      Cgr 
    
    Cgr 
            
       Cgr3         |
13 | | anass 631 |
. . . . . . . . . . 11
        
             
             
               
      
     
   
         
       
          
        |
14 | | simpl11 1032 |
. . . . . . . . . . . . . . 15
       
             
             
          
        |
15 | | simpl21 1035 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
16 | | simprl 733 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
17 | | simpl22 1036 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
18 | | simpl32 1039 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
19 | | simprr 734 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
20 | | simpl33 1040 |
. . . . . . . . . . . . . . 15
       
             
             
          
            |
21 | | brcgr3 25888 |
. . . . . . . . . . . . . . 15
  
   
         
       
             Cgr3     
    Cgr  
   Cgr      Cgr       |
22 | 14, 15, 16, 17, 18, 19, 20, 21 | syl133anc 1207 |
. . . . . . . . . . . . . 14
       
             
             
          
             Cgr3 
        Cgr      Cgr      Cgr       |
23 | 22 | adantr 452 |
. . . . . . . . . . . . 13
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
           Cgr3     
    Cgr  
   Cgr      Cgr       |
24 | | df-3an 938 |
. . . . . . . . . . . . . . 15
      Cgr      Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr           Cgr 
    Cgr 
    
    Cgr 
     
 Cgr 
    Cgr 
    Cgr       |
25 | | simpl23 1037 |
. . . . . . . . . . . . . . . 16
       
             
             
          
            |
26 | | simpl31 1038 |
. . . . . . . . . . . . . . . 16
       
             
             
          
            |
27 | | simpl12 1033 |
. . . . . . . . . . . . . . . . 17
       
             
             
          
            |
28 | | simpl13 1034 |
. . . . . . . . . . . . . . . . 17
       
             
             
          
            |
29 | | simpr1l 1014 |
. . . . . . . . . . . . . . . . 17
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr         Cgr     |
30 | | simpr2r 1017 |
. . . . . . . . . . . . . . . . 17
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr         Cgr     |
31 | 14, 27, 28, 25, 26, 15, 16, 29, 30 | cgrtr4and 25828 |
. . . . . . . . . . . . . . . 16
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr         Cgr     |
32 | | simpr31 1047 |
. . . . . . . . . . . . . . . 16
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr         Cgr     |
33 | 14, 25, 26, 15, 16, 18, 19, 31, 32 | cgrtrand 25835 |
. . . . . . . . . . . . . . 15
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
      Cgr      Cgr      Cgr         Cgr     |
34 | 24, 33 | sylan2br 463 |
. . . . . . . . . . . . . 14
        
             
             
          
            Cgr 
    Cgr 
    
    Cgr 
     
 Cgr 
    Cgr 
    Cgr         Cgr     |
35 | 34 | expr 599 |
. . . . . . . . . . . . 13
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
         Cgr      Cgr      Cgr       Cgr      |
36 | 23, 35 | sylbid 207 |
. . . . . . . . . . . 12
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
           Cgr3         Cgr      |
37 | 36 | anim2d 549 |
. . . . . . . . . . 11
        
             
             
          
         
 Cgr 
    Cgr 
    
    Cgr 
        
      Cgr3 
     
  
   Cgr       |
38 | 13, 37 | sylanb 459 |
. . . . . . . . . 10
     
         
       
             
                     Cgr      Cgr 
    
    Cgr 
        
      Cgr3 
     
  
   Cgr       |
39 | 38 | an32s 780 |
. . . . . . . . 9
     
         
       
             
                Cgr      Cgr 
    
    Cgr 
             
      Cgr3 
     
  
   Cgr       |
40 | 39 | reximdva 2782 |
. . . . . . . 8
        
             
             
                Cgr      Cgr 
    
    Cgr 
     
     
  
      Cgr3 
             
    Cgr 
     |
41 | 12, 40 | mpd 15 |
. . . . . . 7
        
             
             
                Cgr      Cgr 
    
    Cgr 
            
    Cgr 
    |
42 | 41 | expr 599 |
. . . . . 6
        
             
             
               Cgr 
    Cgr 
  
 
  
   Cgr   
        
    Cgr 
     |
43 | 42 | an32s 780 |
. . . . 5
        
             
             
          Cgr 
    Cgr 
            
   Cgr   
        
    Cgr 
     |
44 | 43 | rexlimdva 2794 |
. . . 4
       
             
             
          Cgr 
    Cgr 
  
 
            Cgr   
        
    Cgr 
     |
45 | | simp11 987 |
. . . . . 6
      
     
   
         
       
        |
46 | | simp12 988 |
. . . . . 6
      
     
   
         
       
            |
47 | | simp13 989 |
. . . . . 6
      
     
   
         
       
            |
48 | | simp21 990 |
. . . . . 6
      
     
   
         
       
            |
49 | | simp22 991 |
. . . . . 6
      
     
   
         
       
            |
50 | | brsegle 25950 |
. . . . . 6
  
   
     
   
             
     
  
   Cgr       |
51 | 45, 46, 47, 48, 49, 50 | syl122anc 1193 |
. . . . 5
      
     
   
         
       
           
 
            Cgr       |
52 | 51 | adantr 452 |
. . . 4
       
             
             
          Cgr 
    Cgr 
  
                
   Cgr       |
53 | | simp23 992 |
. . . . . 6
      
     
   
         
       
            |
54 | | simp31 993 |
. . . . . 6
      
     
   
         
       
            |
55 | | simp32 994 |
. . . . . 6
      
     
   
         
       
            |
56 | | simp33 995 |
. . . . . 6
      
     
   
         
       
            |
57 | | brsegle 25950 |
. . . . . 6
  
   
     
   
             
     
  
   Cgr       |
58 | 45, 53, 54, 55, 56, 57 | syl122anc 1193 |
. . . . 5
      
     
   
         
       
           
 
            Cgr       |
59 | 58 | adantr 452 |
. . . 4
       
             
             
          Cgr 
    Cgr 
  
                
   Cgr       |
60 | 44, 52, 59 | 3imtr4d 260 |
. . 3
       
             
             
          Cgr 
    Cgr 
  
      
         |
61 | 60 | exp32 589 |
. 2
      
     
   
         
       
          Cgr 
     Cgr              
      |
62 | 61 | 3impd 1167 |
1
      
     
   
         
       
           Cgr      Cgr 
     
           |