| Step | Hyp | Ref
| Expression |
| 1 | | xpassen.1 |
. . . 4
 |
| 2 | | xpassen.2 |
. . . 4
 |
| 3 | 1, 2 | xpex 4778 |
. . 3
   |
| 4 | | xpassen.3 |
. . 3
 |
| 5 | 3, 4 | xpex 4778 |
. 2
     |
| 6 | 2, 4 | xpex 4778 |
. . 3
   |
| 7 | 1, 6 | xpex 4778 |
. 2
     |
| 8 | | vex 2766 |
. . . . . . . . . 10
 |
| 9 | 8 | snex 4218 |
. . . . . . . . 9
 
 |
| 10 | 9 | dmex 4932 |
. . . . . . . 8
   |
| 11 | 10 | uniex 4472 |
. . . . . . 7
    |
| 12 | 11 | snex 4218 |
. . . . . 6
      |
| 13 | 12 | dmex 4932 |
. . . . 5
    
 |
| 14 | 13 | uniex 4472 |
. . . 4
     
 |
| 15 | 12 | rnex 4933 |
. . . . . 6
    
 |
| 16 | 15 | uniex 4472 |
. . . . 5
     
 |
| 17 | 9 | rnex 4933 |
. . . . . 6
   |
| 18 | 17 | uniex 4472 |
. . . . 5
    |
| 19 | 16, 18 | opex 4262 |
. . . 4
             |
| 20 | 14, 19 | opex 4262 |
. . 3
                      |
| 21 | 20 | a1i 9 |
. 2
                            |
| 22 | | vex 2766 |
. . . . . . . 8
 |
| 23 | 22 | snex 4218 |
. . . . . . 7
   |
| 24 | 23 | dmex 4932 |
. . . . . 6
   |
| 25 | 24 | uniex 4472 |
. . . . 5
    |
| 26 | 23 | rnex 4933 |
. . . . . . . . 9
   |
| 27 | 26 | uniex 4472 |
. . . . . . . 8
    |
| 28 | 27 | snex 4218 |
. . . . . . 7
      |
| 29 | 28 | dmex 4932 |
. . . . . 6
      |
| 30 | 29 | uniex 4472 |
. . . . 5
       |
| 31 | 25, 30 | opex 4262 |
. . . 4
             |
| 32 | 28 | rnex 4933 |
. . . . 5
      |
| 33 | 32 | uniex 4472 |
. . . 4
       |
| 34 | 31, 33 | opex 4262 |
. . 3
              
       |
| 35 | 34 | a1i 9 |
. 2
  
                
        |
| 36 | | sneq 3633 |
. . . . . . . . . . . . . . . . 17
        
          |
| 37 | 36 | dmeqd 4868 |
. . . . . . . . . . . . . . . 16
                   |
| 38 | 37 | unieqd 3850 |
. . . . . . . . . . . . . . 15
                     |
| 39 | 38 | sneqd 3635 |
. . . . . . . . . . . . . 14
                         |
| 40 | 39 | dmeqd 4868 |
. . . . . . . . . . . . 13
           
             |
| 41 | 40 | unieqd 3850 |
. . . . . . . . . . . 12
            
              |
| 42 | | vex 2766 |
. . . . . . . . . . . . . . . . . 18
 |
| 43 | | vex 2766 |
. . . . . . . . . . . . . . . . . 18
 |
| 44 | 42, 43 | opex 4262 |
. . . . . . . . . . . . . . . . 17
  
 |
| 45 | | vex 2766 |
. . . . . . . . . . . . . . . . 17
 |
| 46 | 44, 45 | op1sta 5151 |
. . . . . . . . . . . . . . . 16
             |
| 47 | 46 | sneqi 3634 |
. . . . . . . . . . . . . . 15
                 |
| 48 | 47 | dmeqi 4867 |
. . . . . . . . . . . . . 14
          
      |
| 49 | 48 | unieqi 3849 |
. . . . . . . . . . . . 13
                   |
| 50 | 42, 43 | op1sta 5151 |
. . . . . . . . . . . . 13
       |
| 51 | 49, 50 | eqtri 2217 |
. . . . . . . . . . . 12
             |
| 52 | 41, 51 | eqtr2di 2246 |
. . . . . . . . . . 11
               |
| 53 | 39 | rneqd 4895 |
. . . . . . . . . . . . . 14
           
             |
| 54 | 53 | unieqd 3850 |
. . . . . . . . . . . . 13
            
              |
| 55 | 47 | rneqi 4894 |
. . . . . . . . . . . . . . 15
          
      |
| 56 | 55 | unieqi 3849 |
. . . . . . . . . . . . . 14
                   |
| 57 | 42, 43 | op2nda 5154 |
. . . . . . . . . . . . . 14
       |
| 58 | 56, 57 | eqtri 2217 |
. . . . . . . . . . . . 13
             |
| 59 | 54, 58 | eqtr2di 2246 |
. . . . . . . . . . . 12
               |
| 60 | 36 | rneqd 4895 |
. . . . . . . . . . . . . 14
                   |
| 61 | 60 | unieqd 3850 |
. . . . . . . . . . . . 13
                     |
| 62 | 44, 45 | op2nda 5154 |
. . . . . . . . . . . . 13
          |
| 63 | 61, 62 | eqtr2di 2246 |
. . . . . . . . . . . 12
            |
| 64 | 59, 63 | opeq12d 3816 |
. . . . . . . . . . 11
                        |
| 65 | 52, 64 | opeq12d 3816 |
. . . . . . . . . 10
                                    |
| 66 | | sneq 3633 |
. . . . . . . . . . . . . . 15
                   |
| 67 | 66 | dmeqd 4868 |
. . . . . . . . . . . . . 14
                   |
| 68 | 67 | unieqd 3850 |
. . . . . . . . . . . . 13
                     |
| 69 | 43, 45 | opex 4262 |
. . . . . . . . . . . . . 14
    |
| 70 | 42, 69 | op1sta 5151 |
. . . . . . . . . . . . 13
          |
| 71 | 68, 70 | eqtr2di 2246 |
. . . . . . . . . . . 12
            |
| 72 | 66 | rneqd 4895 |
. . . . . . . . . . . . . . . . 17
                   |
| 73 | 72 | unieqd 3850 |
. . . . . . . . . . . . . . . 16
                     |
| 74 | 73 | sneqd 3635 |
. . . . . . . . . . . . . . 15
                         |
| 75 | 74 | dmeqd 4868 |
. . . . . . . . . . . . . 14
                         |
| 76 | 75 | unieqd 3850 |
. . . . . . . . . . . . 13
                           |
| 77 | 42, 69 | op2nda 5154 |
. . . . . . . . . . . . . . . . 17
             |
| 78 | 77 | sneqi 3634 |
. . . . . . . . . . . . . . . 16
                 |
| 79 | 78 | dmeqi 4867 |
. . . . . . . . . . . . . . 15
                 |
| 80 | 79 | unieqi 3849 |
. . . . . . . . . . . . . 14
                   |
| 81 | 43, 45 | op1sta 5151 |
. . . . . . . . . . . . . 14
     
 |
| 82 | 80, 81 | eqtri 2217 |
. . . . . . . . . . . . 13
             |
| 83 | 76, 82 | eqtr2di 2246 |
. . . . . . . . . . . 12
               |
| 84 | 71, 83 | opeq12d 3816 |
. . . . . . . . . . 11
         
              |
| 85 | 74 | rneqd 4895 |
. . . . . . . . . . . . 13
                         |
| 86 | 85 | unieqd 3850 |
. . . . . . . . . . . 12
                           |
| 87 | 78 | rneqi 4894 |
. . . . . . . . . . . . . 14
                 |
| 88 | 87 | unieqi 3849 |
. . . . . . . . . . . . 13
                   |
| 89 | 43, 45 | op2nda 5154 |
. . . . . . . . . . . . 13
     
 |
| 90 | 88, 89 | eqtri 2217 |
. . . . . . . . . . . 12
             |
| 91 | 86, 90 | eqtr2di 2246 |
. . . . . . . . . . 11
               |
| 92 | 84, 91 | opeq12d 3816 |
. . . . . . . . . 10
                                    |
| 93 | 65, 92 | eq2tri 2256 |
. . . . . . . . 9
       
                     
                               |
| 94 | | anass 401 |
. . . . . . . . 9
  




    |
| 95 | 93, 94 | anbi12i 460 |
. . . . . . . 8
        
                       

 
       
                             |
| 96 | | an32 562 |
. . . . . . . 8
        
 

 
                             
                       

    |
| 97 | | an32 562 |
. . . . . . . 8
        


                                                              |
| 98 | 95, 96, 97 | 3bitr4i 212 |
. . . . . . 7
        
 

 
                             


                           |
| 99 | 98 | exbii 1619 |
. . . . . 6
            

 
                                 
  
              
         |
| 100 | | 19.41v 1917 |
. . . . . 6
            

 
                                 

 
                        |
| 101 | | 19.41v 1917 |
. . . . . 6
            
  
              
                


                           |
| 102 | 99, 100, 101 | 3bitr3i 210 |
. . . . 5
            

 
                                 
  
              
         |
| 103 | 102 | 2exbii 1620 |
. . . 4
                

 
                                     
  
              
         |
| 104 | | 19.41vv 1918 |
. . . 4
                

 
                                     

 
                        |
| 105 | | 19.41vv 1918 |
. . . 4
                
  
              
                    


                           |
| 106 | 103, 104,
105 | 3bitr3i 210 |
. . 3
                

 
                                     
  
              
         |
| 107 | | elxp 4680 |
. . . . 5
    
               |
| 108 | | excom 1678 |
. . . . 5
           
            
    |
| 109 | | elxp 4680 |
. . . . . . . . 9
  
        
    |
| 110 | 109 | anbi1i 458 |
. . . . . . . 8
    
    
            
       |
| 111 | | an12 561 |
. . . . . . . 8
       
    
        |
| 112 | | 19.41vv 1918 |
. . . . . . . 8
          
 
     
            
       |
| 113 | 110, 111,
112 | 3bitr4i 212 |
. . . . . . 7
       
           
          |
| 114 | 113 | 2exbii 1620 |
. . . . . 6
           
               
 
        |
| 115 | | exrot4 1705 |
. . . . . 6
             

 
     
                
       |
| 116 | | anass 401 |
. . . . . . . . 9
      
 
     
                |
| 117 | 116 | exbii 1619 |
. . . . . . . 8
           
    
       

         |
| 118 | | opeq1 3808 |
. . . . . . . . . . . 12
      
        |
| 119 | 118 | eqeq2d 2208 |
. . . . . . . . . . 11
                 |
| 120 | 119 | anbi1d 465 |
. . . . . . . . . 10
                     |
| 121 | 120 | anbi2d 464 |
. . . . . . . . 9
      
      
 
       
     |
| 122 | 44, 121 | ceqsexv 2802 |
. . . . . . . 8
                          
    |
| 123 | | an12 561 |
. . . . . . . 8
  

        
        

    |
| 124 | 117, 122,
123 | 3bitri 206 |
. . . . . . 7
           
    
        

    |
| 125 | 124 | 3exbii 1621 |
. . . . . 6
             

 
     
                    |
| 126 | 114, 115,
125 | 3bitri 206 |
. . . . 5
           
                

    |
| 127 | 107, 108,
126 | 3bitri 206 |
. . . 4
    
                    |
| 128 | 127 | anbi1i 458 |
. . 3
     
                                     

 
                        |
| 129 | | elxp 4680 |
. . . . 5
  
 
        
      |
| 130 | | elxp 4680 |
. . . . . . . . . 10
  
        
    |
| 131 | 130 | anbi2i 457 |
. . . . . . . . 9
         
    
               |
| 132 | | anass 401 |
. . . . . . . . 9
         
           |
| 133 | | 19.42vv 1926 |
. . . . . . . . . 10
               
  
    
               |
| 134 | | an12 561 |
. . . . . . . . . . . 12
           
  
         

     |
| 135 | | anass 401 |
. . . . . . . . . . . . 13
       
       
     |
| 136 | 135 | anbi2i 457 |
. . . . . . . . . . . 12
           
  
         
      |
| 137 | 134, 136 | bitri 184 |
. . . . . . . . . . 11
           
  
         
      |
| 138 | 137 | 2exbii 1620 |
. . . . . . . . . 10
               
  
             
      |
| 139 | 133, 138 | bitr3i 186 |
. . . . . . . . 9
                              
 
      |
| 140 | 131, 132,
139 | 3bitr3i 210 |
. . . . . . . 8
    

               
 
      |
| 141 | 140 | exbii 1619 |
. . . . . . 7
       
                   
      |
| 142 | | exrot3 1704 |
. . . . . . 7
                
                   
      |
| 143 | | opeq2 3809 |
. . . . . . . . . . 11
               |
| 144 | 143 | eqeq2d 2208 |
. . . . . . . . . 10
                 |
| 145 | 144 | anbi1d 465 |
. . . . . . . . 9
                    


      |
| 146 | 69, 145 | ceqsexv 2802 |
. . . . . . . 8
            
          


     |
| 147 | 146 | 2exbii 1620 |
. . . . . . 7
                
              


     |
| 148 | 141, 142,
147 | 3bitri 206 |
. . . . . 6
       
              


     |
| 149 | 148 | exbii 1619 |
. . . . 5
        

                  
     |
| 150 | 129, 149 | bitri 184 |
. . . 4
  
 
            


     |
| 151 | 150 | anbi1i 458 |
. . 3
     
              
                    


                           |
| 152 | 106, 128,
151 | 3bitr4i 212 |
. 2
     
                          
              
         |
| 153 | 5, 7, 21, 35, 152 | en2i 6829 |
1
    
    |