Proof of Theorem lineext
Step | Hyp | Ref
| Expression |
1 | | brcolinear 30838 |
. . . 4
  
   
                   

       |
2 | 1 | 3adant3 1029 |
. . 3
  
   
         
                   

       |
3 | 2 | anbi1d 712 |
. 2
  
   
         
                  Cgr   
         
     Cgr       |
4 | | simp1 1009 |
. . . . . . . . 9
  
   
         
         
  |
5 | | simp3r 1038 |
. . . . . . . . . 10
  
   
         
         
      |
6 | | simp3l 1037 |
. . . . . . . . . 10
  
   
         
         
      |
7 | 5, 6 | jca 535 |
. . . . . . . . 9
  
   
         
                      |
8 | | simp21 1042 |
. . . . . . . . . 10
  
   
         
         
      |
9 | | simp23 1044 |
. . . . . . . . . 10
  
   
         
         
      |
10 | 8, 9 | jca 535 |
. . . . . . . . 9
  
   
         
                      |
11 | 4, 7, 10 | 3jca 1189 |
. . . . . . . 8
  
   
         
                                  |
12 | 11 | adantr 467 |
. . . . . . 7
                            
  
   Cgr     

         
            |
13 | | axsegcon 24969 |
. . . . . . 7
  
   
     
   
               
   Cgr      |
14 | 12, 13 | syl 17 |
. . . . . 6
                            
  
   Cgr             
    Cgr      |
15 | | simprlr 774 |
. . . . . . . . . . 11
            
               
        
    Cgr 
    
    Cgr 
       Cgr     |
16 | | simprrr 776 |
. . . . . . . . . . 11
            
               
        
    Cgr 
    
    Cgr 
       Cgr     |
17 | | an4 834 |
. . . . . . . . . . . . 13
     
   Cgr           Cgr    
             Cgr 
    Cgr 
     |
18 | | simpl1 1012 |
. . . . . . . . . . . . . . . . 17
                           
    
  |
19 | | simpl21 1087 |
. . . . . . . . . . . . . . . . 17
                           
    
      |
20 | | simpl22 1088 |
. . . . . . . . . . . . . . . . 17
                           
    
      |
21 | | simpl3l 1064 |
. . . . . . . . . . . . . . . . 17
                           
    
      |
22 | | simpl3r 1065 |
. . . . . . . . . . . . . . . . 17
                           
    
      |
23 | | cgrcomlr 30777 |
. . . . . . . . . . . . . . . . 17
  
   
     
   
          Cgr      Cgr 
    |
24 | 18, 19, 20, 21, 22, 23 | syl122anc 1278 |
. . . . . . . . . . . . . . . 16
                           
         Cgr      Cgr      |
25 | 24 | anbi1d 712 |
. . . . . . . . . . . . . . 15
                           
          Cgr      Cgr        Cgr      Cgr       |
26 | 25 | anbi2d 711 |
. . . . . . . . . . . . . 14
                           
                   Cgr 
    Cgr 
                Cgr 
    Cgr 
      |
27 | | simpl23 1089 |
. . . . . . . . . . . . . . 15
                           
    
      |
28 | | simpr 463 |
. . . . . . . . . . . . . . 15
                           
           |
29 | | cgrextend 30787 |
. . . . . . . . . . . . . . 15
  
   
         
       
          

        Cgr 
    Cgr 
  
   Cgr      |
30 | 18, 20, 19, 27, 22, 21, 28, 29 | syl133anc 1292 |
. . . . . . . . . . . . . 14
                           
                   Cgr 
    Cgr 
  
   Cgr      |
31 | 26, 30 | sylbid 219 |
. . . . . . . . . . . . 13
                           
                   Cgr 
    Cgr 
  
   Cgr      |
32 | 17, 31 | syl5bi 221 |
. . . . . . . . . . . 12
                           
              Cgr      
    Cgr 
  
   Cgr      |
33 | 32 | imp 431 |
. . . . . . . . . . 11
            
               
        
    Cgr 
    
    Cgr 
       Cgr     |
34 | 15, 16, 33 | 3jca 1189 |
. . . . . . . . . 10
            
               
        
    Cgr 
    
    Cgr 
        Cgr 
    Cgr 
    Cgr 
    |
35 | 34 | expr 620 |
. . . . . . . . 9
            
               
     
  
   Cgr         
   Cgr   
  
 Cgr 
    Cgr 
    Cgr 
     |
36 | | cgrcom 30769 |
. . . . . . . . . . . 12
  
   
     
   
          Cgr      Cgr 
    |
37 | 18, 21, 28, 19, 27, 36 | syl122anc 1278 |
. . . . . . . . . . 11
                           
         Cgr      Cgr 
    |
38 | 37 | anbi2d 711 |
. . . . . . . . . 10
                           
        
    Cgr       
   Cgr       |
39 | 38 | adantr 467 |
. . . . . . . . 9
            
               
     
  
   Cgr         
   Cgr      
    Cgr 
     |
40 | | simpl2 1013 |
. . . . . . . . . . 11
                           
                     |
41 | | brcgr3 30825 |
. . . . . . . . . . 11
  
   
         
       
             Cgr3     
    Cgr  
   Cgr      Cgr       |
42 | 18, 40, 21, 22, 28, 41 | syl113anc 1281 |
. . . . . . . . . 10
                           
            Cgr3          Cgr      Cgr 
    Cgr 
     |
43 | 42 | adantr 467 |
. . . . . . . . 9
            
               
     
  
   Cgr            Cgr3     
    Cgr  
   Cgr      Cgr       |
44 | 35, 39, 43 | 3imtr4d 272 |
. . . . . . . 8
            
               
     
  
   Cgr         
   Cgr   
      Cgr3 
       |
45 | 44 | an32s 814 |
. . . . . . 7
            
                
  
   Cgr              
   Cgr   
      Cgr3 
       |
46 | 45 | reximdva 2864 |
. . . . . 6
                            
  
   Cgr      
     
  
   Cgr   
            Cgr3         |
47 | 14, 46 | mpd 15 |
. . . . 5
                            
  
   Cgr                 Cgr3        |
48 | 47 | exp32 610 |
. . . 4
  
   
         
             
    Cgr  
            Cgr3          |
49 | | 3ancoma 993 |
. . . . . . 7
     
        
    
           |
50 | | btwncom 30793 |
. . . . . . 7
  
   
             
      |
51 | 49, 50 | sylan2b 478 |
. . . . . 6
  
   
             
      |
52 | 51 | 3adant3 1029 |
. . . . 5
  
   
         
             
      |
53 | | simp3 1011 |
. . . . . . . . 9
  
   
         
                      |
54 | | simp22 1043 |
. . . . . . . . 9
  
   
         
         
      |
55 | | axsegcon 24969 |
. . . . . . . . 9
  
   
     
   
               
   Cgr      |
56 | 4, 53, 54, 9, 55 | syl112anc 1273 |
. . . . . . . 8
  
   
         
          
     
  
   Cgr      |
57 | 56 | adantr 467 |
. . . . . . 7
                            
  
   Cgr             
    Cgr      |
58 | | cgrextend 30787 |
. . . . . . . . . . . . 13
  
   
         
       
          

        Cgr 
    Cgr 
  
   Cgr      |
59 | 18, 40, 21, 22, 28, 58 | syl113anc 1281 |
. . . . . . . . . . . 12
                           
                   Cgr 
    Cgr 
  
   Cgr      |
60 | | simpll 761 |
. . . . . . . . . . . . . . 15
      Cgr      Cgr 
     Cgr   
   Cgr     |
61 | | simpr 463 |
. . . . . . . . . . . . . . 15
      Cgr      Cgr 
     Cgr   
   Cgr     |
62 | | simplr 763 |
. . . . . . . . . . . . . . 15
      Cgr      Cgr 
     Cgr   
   Cgr     |
63 | 60, 61, 62 | 3jca 1189 |
. . . . . . . . . . . . . 14
      Cgr      Cgr 
     Cgr   
    Cgr  
   Cgr      Cgr      |
64 | 63 | ex 436 |
. . . . . . . . . . . . 13
     Cgr 
    Cgr 
      Cgr       Cgr      Cgr      Cgr       |
65 | 64 | adantl 468 |
. . . . . . . . . . . 12
     
 
      Cgr      Cgr         Cgr 
     Cgr      Cgr 
    Cgr 
     |
66 | 59, 65 | sylcom 30 |
. . . . . . . . . . 11
                           
                   Cgr 
    Cgr 
  
    Cgr  
   Cgr      Cgr       |
67 | | an4 834 |
. . . . . . . . . . . 12
     
   Cgr           Cgr    
             Cgr 
    Cgr       |
68 | | cgrcom 30769 |
. . . . . . . . . . . . . . 15
  
   
     
   
          Cgr      Cgr 
    |
69 | 18, 22, 28, 20, 27, 68 | syl122anc 1278 |
. . . . . . . . . . . . . 14
                           
         Cgr      Cgr 
    |
70 | 69 | anbi2d 711 |
. . . . . . . . . . . . 13
                           
          Cgr      Cgr        Cgr      Cgr       |
71 | 70 | anbi2d 711 |
. . . . . . . . . . . 12
                           
                   Cgr 
    Cgr                  Cgr 
    Cgr 
      |
72 | 67, 71 | syl5bb 261 |
. . . . . . . . . . 11
                           
              Cgr      
    Cgr                  Cgr 
    Cgr 
      |
73 | 66, 72, 42 | 3imtr4d 272 |
. . . . . . . . . 10
                           
              Cgr      
    Cgr    
      Cgr3 
       |
74 | 73 | expdimp 439 |
. . . . . . . . 9
            
               
     
  
   Cgr         
   Cgr   
      Cgr3 
       |
75 | 74 | an32s 814 |
. . . . . . . 8
            
                
  
   Cgr              
   Cgr   
      Cgr3 
       |
76 | 75 | reximdva 2864 |
. . . . . . 7
                            
  
   Cgr      
     
  
   Cgr   
            Cgr3         |
77 | 57, 76 | mpd 15 |
. . . . . 6
                            
  
   Cgr                 Cgr3        |
78 | 77 | exp32 610 |
. . . . 5
  
   
         
             
    Cgr  
            Cgr3          |
79 | 52, 78 | sylbird 239 |
. . . 4
  
   
         
             
    Cgr  
            Cgr3          |
80 | | cgrxfr 30834 |
. . . . . . 7
  
   
         
             
    Cgr 
           
      Cgr3 
        |
81 | 4, 8, 9, 54, 53, 80 | syl131anc 1282 |
. . . . . 6
  
   
         
             
    Cgr 
           
      Cgr3 
        |
82 | | cgr3permute1 30827 |
. . . . . . . . . 10
  
   
         
       
             Cgr3     
      Cgr3 
       |
83 | 18, 40, 21, 22, 28, 82 | syl113anc 1281 |
. . . . . . . . 9
                           
            Cgr3            Cgr3         |
84 | 83 | biimprd 227 |
. . . . . . . 8
                           
            Cgr3            Cgr3         |
85 | 84 | adantld 469 |
. . . . . . 7
                           
        
       Cgr3             Cgr3         |
86 | 85 | reximdva 2864 |
. . . . . 6
  
   
         
                   
       Cgr3                   Cgr3         |
87 | 81, 86 | syld 45 |
. . . . 5
  
   
         
             
    Cgr 
              Cgr3         |
88 | 87 | expd 438 |
. . . 4
  
   
         
             
    Cgr  
            Cgr3          |
89 | 48, 79, 88 | 3jaod 1334 |
. . 3
  
   
         
             

    
      Cgr               Cgr3          |
90 | 89 | impd 433 |
. 2
  
   
         
                    
     Cgr                Cgr3         |
91 | 3, 90 | sylbid 219 |
1
  
   
         
                  Cgr                Cgr3         |