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

            
    Cgr      
    Cgr      
  
   Cgr           Cgr           |
2 | | simp2rl 1077 |
. . . . . 6
   

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

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         
 
    |
4 | 3 | adantl 468 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         

      |
5 | | simp11 1038 |
. . . . . 6
      
     
   
             
        |
6 | | simp12 1039 |
. . . . . 6
      
     
   
             
            |
7 | | simp13 1040 |
. . . . . 6
      
     
   
             
            |
8 | | simp21 1041 |
. . . . . 6
      
     
   
             
            |
9 | | simp3l 1036 |
. . . . . 6
      
     
   
             
            |
10 | | btwnexch3 30787 |
. . . . . 6
  
   
     
   
                     |
11 | 5, 6, 7, 8, 9, 10 | syl122anc 1277 |
. . . . 5
      
     
   
             
                     |
12 | 11 | adantr 467 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr                      |
13 | 4, 12 | mpd 15 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr            |
14 | | simp3lr 1080 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
15 | 14 | adantl 468 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
16 | | simp23 1043 |
. . . . . . . 8
      
     
   
             
            |
17 | | simp3r 1037 |
. . . . . . . 8
      
     
   
             
            |
18 | | cgrcomlr 30765 |
. . . . . . . 8
                           Cgr      Cgr      |
19 | 5, 16, 17, 8, 7, 18 | syl122anc 1277 |
. . . . . . 7
      
     
   
             
          Cgr      Cgr      |
20 | | cgrcom 30757 |
. . . . . . . 8
                           Cgr      Cgr      |
21 | 5, 17, 16, 7, 8, 20 | syl122anc 1277 |
. . . . . . 7
      
     
   
             
          Cgr      Cgr      |
22 | 19, 21 | bitrd 257 |
. . . . . 6
      
     
   
             
          Cgr      Cgr      |
23 | 22 | adantr 467 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr           Cgr      Cgr      |
24 | 15, 23 | mpbid 214 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
25 | | 3simpa 1005 |
. . . . . 6
       |
26 | 25 | anim1i 572 |
. . . . 5
  

          
            |
27 | | btwnconn1lem3 30856 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
28 | 26, 27 | syl3anr1 1320 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
29 | | simp22 1042 |
. . . . 5
      
     
   
             
            |
30 | | simp2rr 1078 |
. . . . . 6
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
31 | 30 | adantl 468 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
32 | | simp2lr 1076 |
. . . . . . 7
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr         Cgr     |
33 | 32 | adantl 468 |
. . . . . 6
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
34 | 5, 29, 16, 8, 29, 33 | cgrcomland 30766 |
. . . . 5
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
35 | 5, 8, 9, 16, 29, 8, 29, 31, 34 | cgrtr3and 30762 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
36 | | brcgr3 30813 |
. . . . . 6
  
   
             
                 Cgr3          Cgr      Cgr      Cgr       |
37 | 5, 7, 8, 9, 17, 16, 29, 36 | syl133anc 1291 |
. . . . 5
      
     
   
             
             Cgr3          Cgr      Cgr      Cgr       |
38 | 37 | adantr 467 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr              Cgr3          Cgr      Cgr      Cgr       |
39 | 24, 28, 35, 38 | mpbir3and 1191 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr             Cgr3        |
40 | | simpl 459 |
. . . . . . 7
     
           |
41 | | simpr 463 |
. . . . . . 7
     
           |
42 | 40, 41, 41 | 3jca 1188 |
. . . . . 6
     
                     |
43 | 42 | 3anim3i 1196 |
. . . . 5
      
     
   
             
           
             
             
        |
44 | 26 | 3anim1i 1194 |
. . . . 5
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr                      
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
45 | | btwnconn1lem1 30854 |
. . . . 5
       
             
             
        
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
46 | 43, 44, 45 | syl2an 480 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
47 | 5, 8, 16 | cgrrflx2d 30751 |
. . . . 5
      
     
   
             
         Cgr     |
48 | 47 | adantr 467 |
. . . 4
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |
49 | 46, 48 | jca 535 |
. . 3
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr           Cgr      Cgr      |
50 | 13, 39, 49 | 3jca 1188 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         
       Cgr3          Cgr      Cgr       |
51 | | simp1l2 1102 |
. . 3
   

            
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
52 | 51 | adantl 468 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         |
53 | | brofs2 30844 |
. . . . . 6
      
                           
                    
       
      Cgr3     
    Cgr  
   Cgr        |
54 | 53 | anbi1d 711 |
. . . . 5
      
                           
                     
   
            Cgr3     
    Cgr  
   Cgr         |
55 | | 5segofs 30773 |
. . . . 5
      
                           
                     
   

   Cgr      |
56 | 54, 55 | sylbird 239 |
. . . 4
      
                           
          
       Cgr3          Cgr      Cgr         Cgr      |
57 | 5, 7, 8, 9, 16, 17, 16, 29, 8, 56 | syl333anc 1300 |
. . 3
      
     
   
             
        
  
      Cgr3     
    Cgr  
   Cgr         Cgr      |
58 | 57 | adantr 467 |
. 2
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr         
  
      Cgr3     
    Cgr  
   Cgr         Cgr      |
59 | 50, 52, 58 | mp2and 685 |
1
       
             
                                
    Cgr      
    Cgr      
  
   Cgr           Cgr          Cgr     |