Step | Hyp | Ref
| Expression |
1 | | brifs 30858 |
. 2
      
     
   
         
       
                            

        Cgr 
    Cgr 
      Cgr      Cgr        |
2 | | simp1l 1038 |
. . . . . 6
     
 
      Cgr      Cgr        Cgr      Cgr    
 
   |
3 | | simp11 1044 |
. . . . . . 7
      
     
   
         
       
        |
4 | | simp13 1046 |
. . . . . . 7
      
     
   
         
       
            |
5 | | simp21 1047 |
. . . . . . 7
      
     
   
         
       
            |
6 | | axbtwnid 25017 |
. . . . . . 7
 
                |
7 | 3, 4, 5, 6 | syl3anc 1276 |
. . . . . 6
      
     
   
         
       
             |
8 | 2, 7 | syl5 33 |
. . . . 5
      
     
   
         
       
          

        Cgr 
    Cgr 
      Cgr      Cgr    
   |
9 | | simp2r 1041 |
. . . . . . . . 9
     
 
      Cgr      Cgr        Cgr      Cgr    
   Cgr     |
10 | | simp3r 1043 |
. . . . . . . . 9
     
 
      Cgr      Cgr        Cgr      Cgr    
   Cgr     |
11 | 9, 10 | jca 539 |
. . . . . . . 8
     
 
      Cgr      Cgr        Cgr      Cgr    
    Cgr  
   Cgr      |
12 | | opeq2 4180 |
. . . . . . . . . . 11
         |
13 | 12 | breq1d 4425 |
. . . . . . . . . 10
     Cgr 
    Cgr      |
14 | | opeq1 4179 |
. . . . . . . . . . 11
         |
15 | 14 | breq1d 4425 |
. . . . . . . . . 10
     Cgr 
    Cgr      |
16 | 13, 15 | anbi12d 722 |
. . . . . . . . 9
      Cgr      Cgr 
      Cgr      Cgr 
     |
17 | 16 | biimprd 231 |
. . . . . . . 8
      Cgr      Cgr 
      Cgr      Cgr       |
18 | 11, 17 | mpan9 476 |
. . . . . . 7
     

        Cgr 
    Cgr 
      Cgr      Cgr          Cgr 
    Cgr 
    |
19 | | simp31 1050 |
. . . . . . . . . 10
      
     
   
         
       
            |
20 | | simp32 1051 |
. . . . . . . . . 10
      
     
   
         
       
            |
21 | | cgrid2 30818 |
. . . . . . . . . 10
  
   
              Cgr  
   |
22 | 3, 4, 19, 20, 21 | syl13anc 1278 |
. . . . . . . . 9
      
     
   
         
       
          Cgr 

   |
23 | | opeq1 4179 |
. . . . . . . . . . 11
         |
24 | 23 | breq2d 4427 |
. . . . . . . . . 10
     Cgr 
    Cgr      |
25 | 24 | biimprd 231 |
. . . . . . . . 9
     Cgr 
    Cgr 
    |
26 | 22, 25 | syl6 34 |
. . . . . . . 8
      
     
   
         
       
          Cgr 
     Cgr      Cgr 
     |
27 | 26 | impd 437 |
. . . . . . 7
      
     
   
         
       
           Cgr      Cgr 
     Cgr      |
28 | 18, 27 | syl5 33 |
. . . . . 6
      
     
   
         
       
                     Cgr 
    Cgr 
      Cgr      Cgr         Cgr      |
29 | 28 | expd 442 |
. . . . 5
      
     
   
         
       
          

        Cgr 
    Cgr 
      Cgr      Cgr    

   Cgr       |
30 | 8, 29 | mpdd 41 |
. . . 4
      
     
   
         
       
          

        Cgr 
    Cgr 
      Cgr      Cgr    
   Cgr      |
31 | | opeq1 4179 |
. . . . . . . 8
         |
32 | 31 | breq2d 4427 |
. . . . . . 7
    
      |
33 | 32 | anbi1d 716 |
. . . . . 6
     
 
     
 
     |
34 | 31 | breq1d 4425 |
. . . . . . 7
     Cgr 
    Cgr      |
35 | 34 | anbi1d 716 |
. . . . . 6
      Cgr      Cgr 
      Cgr      Cgr 
     |
36 | 33, 35 | 3anbi12d 1349 |
. . . . 5
     

        Cgr 
    Cgr 
      Cgr      Cgr                  Cgr 
    Cgr 
      Cgr      Cgr        |
37 | 36 | imbi1d 323 |
. . . 4
                Cgr 
    Cgr 
      Cgr      Cgr    
   Cgr      
  
 
      Cgr      Cgr        Cgr      Cgr    
   Cgr       |
38 | 30, 37 | syl5ibr 229 |
. . 3
       
             
             
          

        Cgr 
    Cgr 
      Cgr      Cgr    
   Cgr       |
39 | | simp12 1045 |
. . . . . . 7
      
     
   
         
       
            |
40 | | btwndiff 30842 |
. . . . . . 7
 
                 
    |
41 | 3, 39, 5, 40 | syl3anc 1276 |
. . . . . 6
      
     
   
         
       
              
    |
42 | | simpl11 1089 |
. . . . . . . . . 10
       
             
             
             |
43 | | simpl23 1094 |
. . . . . . . . . 10
       
             
             
                 |
44 | | simpl32 1096 |
. . . . . . . . . 10
       
             
             
                 |
45 | | simpl21 1092 |
. . . . . . . . . 10
       
             
             
                 |
46 | | simpr 467 |
. . . . . . . . . 10
       
             
             
                 |
47 | | axsegcon 25005 |
. . . . . . . . . 10
  
   
     
   
               
   Cgr      |
48 | 42, 43, 44, 45, 46, 47 | syl122anc 1285 |
. . . . . . . . 9
       
             
             
                   
    Cgr      |
49 | | anass 659 |
. . . . . . . . . . . . 13
     
    Cgr   
          

        Cgr 
    Cgr 
      Cgr      Cgr      
        Cgr   
    
     

        Cgr 
    Cgr 
      Cgr      Cgr          |
50 | | anass 659 |
. . . . . . . . . . . . . 14
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr      
     
   Cgr   
          

        Cgr 
    Cgr 
      Cgr      Cgr         |
51 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . 21
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           |
52 | 51 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr            |
53 | | simplll 773 |
. . . . . . . . . . . . . . . . . . . . 21
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           |
54 | 53 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr            |
55 | 52, 54 | jca 539 |
. . . . . . . . . . . . . . . . . . 19
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          
 
    |
56 | | simpr2l 1073 |
. . . . . . . . . . . . . . . . . . . . 21
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr     |
57 | 56 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          Cgr 
   |
58 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr     |
59 | 58 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          Cgr     |
60 | 3 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr      
  |
61 | 20 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr      
      |
62 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr             |
63 | 5 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr      
      |
64 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr             |
65 | | cgrcom 30805 |
. . . . . . . . . . . . . . . . . . . . . 22
  
   
     
   
          Cgr      Cgr      |
66 | 60, 61, 62, 63, 64, 65 | syl122anc 1285 |
. . . . . . . . . . . . . . . . . . . . 21
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           Cgr      Cgr      |
67 | 59, 66 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          Cgr     |
68 | 57, 67 | jca 539 |
. . . . . . . . . . . . . . . . . . 19
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           Cgr      Cgr      |
69 | | simprr3 1064 |
. . . . . . . . . . . . . . . . . . 19
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           Cgr      Cgr 
    |
70 | 55, 68, 69 | 3jca 1194 |
. . . . . . . . . . . . . . . . . 18
        
             
             
          
        
  
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          

        Cgr 
    Cgr   
    Cgr  
   Cgr       |
71 | 70 | ex 440 |
. . . . . . . . . . . . . . . . 17
       
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          
 
      Cgr      Cgr   
    Cgr 
    Cgr 
      |
72 | | simpl11 1089 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
        |
73 | | simpl12 1090 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
74 | | simpl21 1092 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
75 | | simprl 769 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
76 | | simpl22 1093 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
77 | | simpl23 1094 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
78 | | simpl32 1096 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
79 | | simprr 771 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
80 | | simpl33 1097 |
. . . . . . . . . . . . . . . . . 18
       
             
             
          
            |
81 | | brofs 30820 |
. . . . . . . . . . . . . . . . . 18
      
                           
                            

        Cgr 
    Cgr   
    Cgr  
   Cgr        |
82 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 81 | syl333anc 1308 |
. . . . . . . . . . . . . . . . 17
       
             
             
          
                            

        Cgr 
    Cgr   
    Cgr  
   Cgr        |
83 | 71, 82 | sylibrd 242 |
. . . . . . . . . . . . . . . 16
       
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr                           |
84 | | 5segofs 30821 |
. . . . . . . . . . . . . . . . 17
      
                           
                         

   Cgr      |
85 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 84 | syl333anc 1308 |
. . . . . . . . . . . . . . . 16
       
             
             
          
                   
     

   Cgr      |
86 | 83, 85 | syland 488 |
. . . . . . . . . . . . . . 15
       
             
             
          
            
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr          Cgr      |
87 | | simpr1l 1071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           |
88 | 87 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         |
89 | 51 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         |
90 | 88, 89 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr              |
91 | | simpr1r 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr           |
92 | 91 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         |
93 | 53 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         |
94 | 90, 92, 93 | jca32 542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        
 
    

       |
95 | | simpl13 1091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
             
             
          
            |
96 | | btwnexch3 30835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   
     
   
                     |
97 | 72, 73, 95, 74, 75, 96 | syl122anc 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             
             
          
                     |
98 | | simpl31 1095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
             
             
          
            |
99 | | btwnexch3 30835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   
     
   
                     |
100 | 72, 77, 98, 78, 79, 99 | syl122anc 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             
             
          
                     |
101 | 97, 100 | anim12d 570 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
             
             
          
        
  
 
    

        
 
     |
102 | 94, 101 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
             
             
          
            
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr               |
103 | 102 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        
 
    |
104 | | btwncom 30829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
   
             
      |
105 | 72, 74, 95, 75, 104 | syl13anc 1278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
             
             
          
        
       |
106 | | btwncom 30829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
   
             
      |
107 | 72, 78, 98, 79, 106 | syl13anc 1278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
             
             
          
        
       |
108 | 105, 107 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
             
             
          
              
           |
109 | 108 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        

   
           |
110 | 103, 109 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        
      |
111 | 58 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr     |
112 | 72, 78, 79, 74, 75, 65 | syl122anc 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             
             
          
          Cgr      Cgr      |
113 | | cgrcomlr 30813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   
     
   
          Cgr      Cgr      |
114 | 72, 74, 75, 78, 79, 113 | syl122anc 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             
             
          
          Cgr      Cgr      |
115 | 112, 114 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
             
             
          
          Cgr      Cgr      |
116 | 115 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         Cgr      Cgr      |
117 | 111, 116 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr     |
118 | | simpr2r 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr     |
119 | 118 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr 
   |
120 | 72, 95, 74, 98, 78, 119 | cgrcomlrand 30816 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr 
   |
121 | 117, 120 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr         Cgr      Cgr 
    |
122 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr     |
123 | | simpr3r 1076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
    Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr     |
124 | 123 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         Cgr        Cgr 
   |
125 | 122, 124 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . 22
        
             
             
          
            
   Cgr   
          
 
      Cgr      Cgr        Cgr      Cgr         |