Step | Hyp | Ref
| Expression |
1 | | df-ne 2643 |
. . 3

  |
2 | | simp2rl 1099 |
. . . . . . . . . 10
   
             
    Cgr      
    Cgr      
  
   Cgr           Cgr           |
3 | 2 | adantr 472 |
. . . . . . . . 9
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr            |
4 | | simp2ll 1097 |
. . . . . . . . . 10
   
             
    Cgr      
    Cgr      
  
   Cgr           Cgr           |
5 | 4 | adantr 472 |
. . . . . . . . 9
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr            |
6 | 3, 5 | jca 541 |
. . . . . . . 8
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    |
7 | | simpl1 1033 |
. . . . . . . . . 10
      
          
                       |
8 | | simprl1 1075 |
. . . . . . . . . 10
      
          
                           |
9 | | simpl2 1034 |
. . . . . . . . . 10
      
          
                           |
10 | | simprrl 782 |
. . . . . . . . . 10
      
          
                           |
11 | | btwncom 30852 |
. . . . . . . . . 10
  
   
             
      |
12 | 7, 8, 9, 10, 11 | syl13anc 1294 |
. . . . . . . . 9
      
          
                       
       |
13 | | simprl2 1076 |
. . . . . . . . . 10
      
          
                           |
14 | | simprl3 1077 |
. . . . . . . . . 10
      
          
                           |
15 | | btwncom 30852 |
. . . . . . . . . 10
  
   
             
      |
16 | 7, 13, 9, 14, 15 | syl13anc 1294 |
. . . . . . . . 9
      
          
                       
       |
17 | 12, 16 | anbi12d 725 |
. . . . . . . 8
      
          
                             
           |
18 | 6, 17 | syl5ib 227 |
. . . . . . 7
      
          
                         
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
       |
19 | | axpasch 25050 |
. . . . . . . 8
                               
            

       |
20 | 7, 10, 14, 9, 8, 13, 19 | syl132anc 1310 |
. . . . . . 7
      
          
                                      

       |
21 | 18, 20 | syld 44 |
. . . . . 6
      
          
                         
             
    Cgr      
    Cgr      
  
   Cgr           Cgr       
     
  
 
     |
22 | 21 | imp 436 |
. . . . 5
       
          
             
          
             
    Cgr      
    Cgr      
  
   Cgr           Cgr                 
 
    |
23 | | simpll1 1069 |
. . . . . . . . . 10
       
          
             
              |
24 | 14 | adantr 472 |
. . . . . . . . . 10
       
          
             
                  |
25 | 8 | adantr 472 |
. . . . . . . . . 10
       
          
             
                  |
26 | 10 | adantr 472 |
. . . . . . . . . 10
       
          
             
                  |
27 | | axsegcon 25036 |
. . . . . . . . . 10
                       
     
  
   Cgr      |
28 | 23, 24, 25, 25, 26, 27 | syl122anc 1301 |
. . . . . . . . 9
       
          
             
                         Cgr 
    |
29 | | simpr 468 |
. . . . . . . . . 10
       
          
             
                  |
30 | | axsegcon 25036 |
. . . . . . . . . 10
                       
     
  
   Cgr      |
31 | 23, 26, 25, 25, 29, 30 | syl122anc 1301 |
. . . . . . . . 9
       
          
             
                         Cgr      |
32 | | reeanv 2944 |
. . . . . . . . 9
                 
   Cgr   
       Cgr    
 
            Cgr   
             Cgr       |
33 | 28, 31, 32 | sylanbrc 677 |
. . . . . . . 8
       
          
             
                                Cgr   
       Cgr       |
34 | 33 | adantr 472 |
. . . . . . 7
        
          
             
                  
  
 
    
  
   Cgr           Cgr         
   Cgr           Cgr          
 
                        Cgr   
       Cgr       |
35 | 7 | ad2antrr 740 |
. . . . . . . . . . . . 13
        
          
             
                
        |
36 | | simprl 772 |
. . . . . . . . . . . . 13
        
          
             
                
            |
37 | | simprr 774 |
. . . . . . . . . . . . 13
        
          
             
                
            |
38 | | axsegcon 25036 |
. . . . . . . . . . . . 13
  
   
                             Cgr      |
39 | 35, 36, 37, 37, 36, 38 | syl122anc 1301 |
. . . . . . . . . . . 12
        
          
             
                
                   Cgr      |
40 | 39 | adantr 472 |
. . . . . . . . . . 11
     
                                                         
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr                    Cgr      |
41 | | simp-4l 784 |
. . . . . . . . . . . . . 14
     
                                                   
         
       |
42 | | simplrl 778 |
. . . . . . . . . . . . . . . 16
       
          
             
            
       
       |
43 | 42 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
     
                                                   
                     |
44 | 10 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
     
                                                   
           |
45 | | simprrr 783 |
. . . . . . . . . . . . . . . . 17
      
          
                           |
46 | 45 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
     
                                                   
           |
47 | | simpllr 777 |
. . . . . . . . . . . . . . . 16
     
                                                   
           |
48 | 44, 46, 47 | 3jca 1210 |
. . . . . . . . . . . . . . 15
     
                                                   
                     |
49 | 43, 48 | jca 541 |
. . . . . . . . . . . . . 14
     
                                                   
          
                 
        |
50 | | simplrl 778 |
. . . . . . . . . . . . . . 15
     
                                                   
    
      |
51 | | simpr 468 |
. . . . . . . . . . . . . . 15
     
                                                   
           |
52 | | simplrr 779 |
. . . . . . . . . . . . . . 15
     
                                                   
           |
53 | 50, 51, 52 | 3jca 1210 |
. . . . . . . . . . . . . 14
     
                                                   
                     |
54 | 41, 49, 53 | 3jca 1210 |
. . . . . . . . . . . . 13
     
                                                   
          
          
             
          
   
            |
55 | | simp1ll 1093 |
. . . . . . . . . . . . . . . . . . 19
   
             
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
56 | 55 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
      

            
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr        |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr       |
58 | | simp1lr 1094 |
. . . . . . . . . . . . . . . . . . 19
   
             
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
59 | 58 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
      

            
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr        |
60 | 59 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr       |
61 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
      

            
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr        |
62 | 61 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr       |
63 | 57, 60, 62 | 3jca 1210 |
. . . . . . . . . . . . . . . 16
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr     
   |
64 | | simpl1r 1082 |
. . . . . . . . . . . . . . . . 17
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    |
65 | 64 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
 
    |
66 | 63, 65 | jca 541 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr      

           |
67 | | simpll2 1070 |
. . . . . . . . . . . . . . . 16
       
  
 
    
  
   Cgr           Cgr         
   Cgr           Cgr          
 
  
        Cgr           Cgr       |
68 | 67 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
    Cgr      
    Cgr       |
69 | | simpl3l 1085 |
. . . . . . . . . . . . . . . . 17
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr          
   Cgr      |
70 | 69 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
   Cgr      |
71 | | simpl3r 1086 |
. . . . . . . . . . . . . . . . 17
                  
    Cgr      
    Cgr      
  
   Cgr           Cgr          
   Cgr      |
72 | 71 | ad3antrrr 744 |
. . . . . . . . . . . . . . . 16
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
   Cgr      |
73 | 70, 72 | jca 541 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
    Cgr      
    Cgr       |
74 | 66, 68, 73 | 3jca 1210 |
. . . . . . . . . . . . . 14
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr                     
    Cgr      
    Cgr      
  
   Cgr           Cgr        |
75 | | simpllr 777 |
. . . . . . . . . . . . . 14
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
 
    |
76 | | simplrl 778 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        
   Cgr      |
77 | | simplrr 779 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr            Cgr      |
78 | | simpr 468 |
. . . . . . . . . . . . . . 15
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr            Cgr      |
79 | 76, 77, 78 | 3jca 1210 |
. . . . . . . . . . . . . 14
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr             Cgr 
         Cgr   

  
   Cgr       |
80 | 74, 75, 79 | jca32 544 |
. . . . . . . . . . . . 13
       
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr                      
    Cgr      
    Cgr      
  
   Cgr           Cgr         

        
   Cgr   
       Cgr   

  
   Cgr         |
81 | | btwnconn1lem12 30936 |
. . . . . . . . . . . . 13
       
          
             
          
   
                           
    Cgr      
    Cgr      
  
   Cgr           Cgr         

        
   Cgr   
       Cgr   

  
   Cgr          |
82 | 54, 80, 81 | syl2an 485 |
. . . . . . . . . . . 12
          
          
                                    
                         
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr             Cgr        |
83 | 82 | an4s 842 |
. . . . . . . . . . 11
          
          
                                          
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr           
       Cgr     
  |
84 | 40, 83 | rexlimddv 2875 |
. . . . . . . . . 10
     
                                                         
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
    
  
   Cgr   
       Cgr         |
85 | 84 | an4s 842 |
. . . . . . . . 9
     
                                                           
    Cgr      
    Cgr      
  
   Cgr           Cgr          
 
                
  
   Cgr   
       Cgr         |
86 | 85 | exp32 616 |
. . . . . . . 8
        
          
             
                  
  
 
    
  
   Cgr           Cgr         
   Cgr           Cgr          
 
              
     
   Cgr   
       Cgr         |
87 | 86 | rexlimdvv 2877 |
. . . . . . 7
        
          
             
                  
  
 
    
  
   Cgr           Cgr         
   Cgr           Cgr          
 
     
               
   Cgr   
       Cgr        |
88 | 34, 87 | mpd 15 |
. . . . . 6
        
          
             
                  
  
 
    
  
   Cgr           Cgr         
   Cgr           Cgr          
 
      |
89 | 88 | an4s 842 |
. . . . 5
        
          
             
          
             
    Cgr      
    Cgr      
  
   Cgr           Cgr            
            |
90 | 22, 89 | rexlimddv 2875 |
. . . 4
       
          
             
          
             
    Cgr      
    Cgr      
  
   Cgr           Cgr          |
91 | 90 | expr 626 |
. . 3
       
          
             
         

            
    Cgr      
    Cgr      
  
   Cgr           Cgr       
   |
92 | 1, 91 | syl5bir 226 |
. 2
       
          
             
         

            
    Cgr      
    Cgr      
  
   Cgr           Cgr       
   |
93 | 92 | orrd 385 |
1
       
          
             
         

            
    Cgr      
    Cgr      
  
   Cgr           Cgr           |