Proof of Theorem btwnconn1lem4
Step | Hyp | Ref
| Expression |
1 | | simp1rl 1053 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr           |
2 | | simp2rl 1057 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr           |
3 | 1, 2 | jca 532 |
. . . . 5
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         
 
    |
4 | 3 | adantl 466 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         

      |
5 | | simp11 1018 |
. . . . . 6
      
     
   
             
        |
6 | | simp12 1019 |
. . . . . 6
      
     
   
             
            |
7 | | simp13 1020 |
. . . . . 6
      
     
   
             
            |
8 | | simp21 1021 |
. . . . . 6
      
     
   
             
            |
9 | | simp3l 1016 |
. . . . . 6
      
     
   
             
            |
10 | | btwnexch3 28185 |
. . . . . 6
  
   
     
   
                     |
11 | 5, 6, 7, 8, 9, 10 | syl122anc 1228 |
. . . . 5
      
     
   
             
                     |
12 | 11 | adantr 465 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr                      |
13 | 4, 12 | mpd 15 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr            |
14 | | simp3lr 1060 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
15 | 14 | adantl 466 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
16 | | simp23 1023 |
. . . . . . . 8
      
     
   
             
            |
17 | | simp3r 1017 |
. . . . . . . 8
      
     
   
             
            |
18 | | cgrcomlr 28163 |
. . . . . . . 8
                           Cgr      Cgr      |
19 | 5, 16, 17, 8, 7, 18 | syl122anc 1228 |
. . . . . . 7
      
     
   
             
          Cgr      Cgr      |
20 | | cgrcom 28155 |
. . . . . . . 8
                           Cgr      Cgr      |
21 | 5, 17, 16, 7, 8, 20 | syl122anc 1228 |
. . . . . . 7
      
     
   
             
          Cgr      Cgr      |
22 | 19, 21 | bitrd 253 |
. . . . . 6
      
     
   
             
          Cgr      Cgr      |
23 | 22 | adantr 465 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr           Cgr      Cgr      |
24 | 15, 23 | mpbid 210 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
25 | | 3simpa 985 |
. . . . . 6
       |
26 | 25 | anim1i 568 |
. . . . 5
  

          
            |
27 | | btwnconn1lem3 28254 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
28 | 26, 27 | syl3anr1 1271 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
29 | | simp22 1022 |
. . . . 5
      
     
   
             
            |
30 | | simp2rr 1058 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
31 | 30 | adantl 466 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
32 | | simp2lr 1056 |
. . . . . . 7
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
33 | 32 | adantl 466 |
. . . . . 6
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
34 | 5, 29, 16, 8, 29, 33 | cgrcomland 28164 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
35 | 5, 8, 9, 16, 29, 8, 29, 31, 34 | cgrtr3and 28160 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
36 | | brcgr3 28211 |
. . . . . 6
  
   
             
                 Cgr3          Cgr      Cgr      Cgr       |
37 | 5, 7, 8, 9, 17, 16, 29, 36 | syl133anc 1242 |
. . . . 5
      
     
   
             
             Cgr3          Cgr      Cgr      Cgr       |
38 | 37 | adantr 465 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr              Cgr3          Cgr      Cgr      Cgr       |
39 | 24, 28, 35, 38 | mpbir3and 1171 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr             Cgr3        |
40 | | simpl 457 |
. . . . . . 7
     
           |
41 | | simpr 461 |
. . . . . . 7
     
           |
42 | 40, 41, 41 | 3jca 1168 |
. . . . . 6
     
                     |
43 | 42 | 3anim3i 1176 |
. . . . 5
      
     
   
             
           
             
             
        |
44 | 26 | 3anim1i 1174 |
. . . . 5
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr                      
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
45 | | btwnconn1lem1 28252 |
. . . . 5
       
             
             
        
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
46 | 43, 44, 45 | syl2an 477 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
47 | 5, 8, 16 | cgrrflx2d 28149 |
. . . . 5
      
     
   
             
         Cgr     |
48 | 47 | adantr 465 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
49 | 46, 48 | jca 532 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr           Cgr      Cgr      |
50 | 13, 39, 49 | 3jca 1168 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         
       Cgr3          Cgr      Cgr       |
51 | | simp1l2 1082 |
. . 3
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
52 | 51 | adantl 466 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         |
53 | | brofs2 28242 |
. . . . . 6
      
                           
                    
       
      Cgr3     
    Cgr  
   Cgr        |
54 | 53 | anbi1d 704 |
. . . . 5
      
                           
                     
   
            Cgr3     
    Cgr  
   Cgr         |
55 | | 5segofs 28171 |
. . . . 5
      
                           
                     
   

   Cgr      |
56 | 54, 55 | sylbird 235 |
. . . 4
      
                           
          
       Cgr3          Cgr      Cgr         Cgr      |
57 | 5, 7, 8, 9, 16, 17, 16, 29, 8, 56 | syl333anc 1251 |
. . 3
      
     
   
             
        
  
      Cgr3     
    Cgr  
   Cgr         Cgr      |
58 | 57 | adantr 465 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         
  
      Cgr3     
    Cgr  
   Cgr         Cgr      |
59 | 50, 52, 58 | mp2and 679 |
1
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |