Proof of Theorem fscgr
Step | Hyp | Ref
| Expression |
1 | | brfs 30846 |
. . 3
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
2 | 1 | anbi1d 711 |
. 2
      
     
   
         
       
                         
            Cgr3          Cgr 
    Cgr 
       |
3 | | simp11 1038 |
. . . . . 6
      
     
   
         
       
        |
4 | | simp12 1039 |
. . . . . 6
      
     
   
         
       
            |
5 | | simp13 1040 |
. . . . . 6
      
     
   
         
       
            |
6 | | simp21 1041 |
. . . . . 6
      
     
   
         
       
            |
7 | | brcolinear 30826 |
. . . . . 6
  
   
                   

       |
8 | 3, 4, 5, 6, 7 | syl13anc 1270 |
. . . . 5
      
     
   
         
       
               

       |
9 | | simp23 1043 |
. . . . . . . . . . . . 13
      
     
   
         
       
            |
10 | | simp31 1044 |
. . . . . . . . . . . . 13
      
     
   
         
       
            |
11 | | simp32 1045 |
. . . . . . . . . . . . 13
      
     
   
         
       
            |
12 | | cgr3permute2 30816 |
. . . . . . . . . . . . 13
  
   
         
       
             Cgr3     
      Cgr3 
       |
13 | 3, 4, 5, 6, 9, 10,
11, 12 | syl133anc 1291 |
. . . . . . . . . . . 12
      
     
   
         
       
             Cgr3     
      Cgr3 
       |
14 | | ancom 452 |
. . . . . . . . . . . . 13
     Cgr 
    Cgr 
      Cgr      Cgr 
    |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
      
     
   
         
       
           Cgr      Cgr 
      Cgr      Cgr 
     |
16 | 13, 15 | 3anbi23d 1342 |
. . . . . . . . . . 11
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
          Cgr3          Cgr      Cgr 
      |
17 | | simp22 1042 |
. . . . . . . . . . . 12
      
     
   
         
       
            |
18 | | simp33 1046 |
. . . . . . . . . . . 12
      
     
   
         
       
            |
19 | | brofs2 30844 |
. . . . . . . . . . . 12
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
20 | 3, 5, 4, 6, 17, 10, 9, 11, 18, 19 | syl333anc 1300 |
. . . . . . . . . . 11
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
21 | 16, 20 | bitr4d 260 |
. . . . . . . . . 10
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
                     |
22 | | necom 2677 |
. . . . . . . . . . 11

  |
23 | 22 | a1i 11 |
. . . . . . . . . 10
      
     
   
         
       
      
   |
24 | 21, 23 | anbi12d 717 |
. . . . . . . . 9
      
     
   
         
       
          
       Cgr3          Cgr 
    Cgr 
   
   
        
     
    |
25 | | 5segofs 30773 |
. . . . . . . . . 10
      
     
   
         
       
                         

   Cgr      |
26 | 3, 5, 4, 6, 17, 10, 9, 11, 18, 25 | syl333anc 1300 |
. . . . . . . . 9
      
     
   
         
       
                         

   Cgr      |
27 | 24, 26 | sylbid 219 |
. . . . . . . 8
      
     
   
         
       
          
       Cgr3          Cgr 
    Cgr 
       Cgr      |
28 | 27 | expd 438 |
. . . . . . 7
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr         Cgr       |
29 | 28 | 3expd 1226 |
. . . . . 6
      
     
   
         
       
                 Cgr3 
   
     Cgr 
    Cgr 
  
   Cgr         |
30 | | btwncom 30781 |
. . . . . . . . . . . . 13
  
   
             
      |
31 | 3, 5, 6, 4, 30 | syl13anc 1270 |
. . . . . . . . . . . 12
      
     
   
         
       
         
      |
32 | 31 | 3anbi1d 1343 |
. . . . . . . . . . 11
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
          Cgr3          Cgr      Cgr 
      |
33 | | brofs2 30844 |
. . . . . . . . . . 11
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
34 | 32, 33 | bitr4d 260 |
. . . . . . . . . 10
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
                     |
35 | 34 | anbi1d 711 |
. . . . . . . . 9
      
     
   
         
       
          
       Cgr3          Cgr 
    Cgr 
   
   
        
     
    |
36 | | 5segofs 30773 |
. . . . . . . . 9
      
     
   
         
       
                         

   Cgr      |
37 | 35, 36 | sylbid 219 |
. . . . . . . 8
      
     
   
         
       
          
       Cgr3          Cgr 
    Cgr 
       Cgr      |
38 | 37 | expd 438 |
. . . . . . 7
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr         Cgr       |
39 | 38 | 3expd 1226 |
. . . . . 6
      
     
   
         
       
                 Cgr3 
   
     Cgr 
    Cgr 
  
   Cgr         |
40 | | cgr3permute1 30815 |
. . . . . . . . . . . 12
  
   
         
       
             Cgr3     
      Cgr3 
       |
41 | 3, 4, 5, 6, 9, 10,
11, 40 | syl133anc 1291 |
. . . . . . . . . . 11
      
     
   
         
       
             Cgr3     
      Cgr3 
       |
42 | 41 | 3anbi2d 1344 |
. . . . . . . . . 10
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
          Cgr3          Cgr      Cgr 
      |
43 | | brifs2 30845 |
. . . . . . . . . . 11
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
44 | 3, 4, 6, 5, 17, 9,
11, 10, 18, 43 | syl333anc 1300 |
. . . . . . . . . 10
      
     
   
         
       
                            
      Cgr3 
   
    Cgr  
   Cgr        |
45 | 42, 44 | bitr4d 260 |
. . . . . . . . 9
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr    
                     |
46 | | ifscgr 30811 |
. . . . . . . . . 10
      
     
   
         
       
                        
   Cgr      |
47 | 3, 4, 6, 5, 17, 9,
11, 10, 18, 46 | syl333anc 1300 |
. . . . . . . . 9
      
     
   
         
       
                        
   Cgr      |
48 | 45, 47 | sylbid 219 |
. . . . . . . 8
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr        Cgr      |
49 | 48 | a1dd 47 |
. . . . . . 7
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr         Cgr       |
50 | 49 | 3expd 1226 |
. . . . . 6
      
     
   
         
       
                 Cgr3 
   
     Cgr 
    Cgr 
  
   Cgr         |
51 | 29, 39, 50 | 3jaod 1332 |
. . . . 5
      
     
   
         
       
            

           Cgr3           Cgr      Cgr 
  
   Cgr         |
52 | 8, 51 | sylbid 219 |
. . . 4
      
     
   
         
       
                 Cgr3 
   
     Cgr 
    Cgr 
  
   Cgr         |
53 | 52 | 3impd 1223 |
. . 3
      
     
   
         
       
          
      Cgr3 
   
    Cgr  
   Cgr         Cgr       |
54 | 53 | impd 433 |
. 2
      
     
   
         
       
                  Cgr3          Cgr 
    Cgr 
       Cgr      |
55 | 2, 54 | sylbid 219 |
1
      
     
   
         
       
                         

   Cgr      |