Step | Hyp | Ref
| Expression |
1 | | dff12 5420 |
. 2
    
             |
2 | | ffn 5365 |
. . . 4
    
  |
3 | | vex 2740 |
. . . . . . . . . . . . . . 15
 |
4 | | vex 2740 |
. . . . . . . . . . . . . . 15
 |
5 | 3, 4 | breldm 4831 |
. . . . . . . . . . . . . 14
     |
6 | | fndm 5315 |
. . . . . . . . . . . . . . 15
   |
7 | 6 | eleq2d 2247 |
. . . . . . . . . . . . . 14
     |
8 | 5, 7 | imbitrid 154 |
. . . . . . . . . . . . 13
   
   |
9 | | vex 2740 |
. . . . . . . . . . . . . . 15
 |
10 | 9, 4 | breldm 4831 |
. . . . . . . . . . . . . 14
     |
11 | 6 | eleq2d 2247 |
. . . . . . . . . . . . . 14
     |
12 | 10, 11 | imbitrid 154 |
. . . . . . . . . . . . 13
       |
13 | 8, 12 | anim12d 335 |
. . . . . . . . . . . 12
       

    |
14 | 13 | pm4.71rd 394 |
. . . . . . . . . . 11
                     |
15 | | eqcom 2179 |
. . . . . . . . . . . . . . 15
    
      |
16 | | fnbrfvb 5556 |
. . . . . . . . . . . . . . 15
 
           |
17 | 15, 16 | bitrid 192 |
. . . . . . . . . . . . . 14
 
           |
18 | | eqcom 2179 |
. . . . . . . . . . . . . . 15
    
      |
19 | | fnbrfvb 5556 |
. . . . . . . . . . . . . . 15
 
           |
20 | 18, 19 | bitrid 192 |
. . . . . . . . . . . . . 14
 
           |
21 | 17, 20 | bi2anan9 606 |
. . . . . . . . . . . . 13
  


       
              |
22 | 21 | anandis 592 |
. . . . . . . . . . . 12
  
                      |
23 | 22 | pm5.32da 452 |
. . . . . . . . . . 11
         
                   |
24 | 14, 23 | bitr4d 191 |
. . . . . . . . . 10
               
         |
25 | 24 | imbi1d 231 |
. . . . . . . . 9
         
  

               |
26 | | impexp 263 |
. . . . . . . . 9
         
                    
    |
27 | 25, 26 | bitrdi 196 |
. . . . . . . 8
         
 
      
    
     |
28 | 27 | albidv 1824 |
. . . . . . 7
          
                
     |
29 | | 19.21v 1873 |
. . . . . . . 8
                
 
 
        
    
    |
30 | | 19.23v 1883 |
. . . . . . . . . . 11
             
             
   |
31 | | funfvex 5532 |
. . . . . . . . . . . . . 14
         |
32 | 31 | funfni 5316 |
. . . . . . . . . . . . 13
 
       |
33 | | eqvincg 2861 |
. . . . . . . . . . . . 13
             
               |
34 | 32, 33 | syl 14 |
. . . . . . . . . . . 12
 
                
        |
35 | 34 | imbi1d 231 |
. . . . . . . . . . 11
 
          

       
    
    |
36 | 30, 35 | bitr4id 199 |
. . . . . . . . . 10
 
              

             |
37 | 36 | adantrr 479 |
. . . . . . . . 9
  
               
         
    |
38 | 37 | pm5.74da 443 |
. . . . . . . 8
            
    
 
 
               |
39 | 29, 38 | bitrid 192 |
. . . . . . 7
                 
 
 
               |
40 | 28, 39 | bitrd 188 |
. . . . . 6
          
  

              |
41 | 40 | 2albidv 1867 |
. . . . 5
              
      

              |
42 | | breq1 4006 |
. . . . . . . 8
   
     |
43 | 42 | mo4 2087 |
. . . . . . 7
              
   |
44 | 43 | albii 1470 |
. . . . . 6
                  
   |
45 | | alrot3 1485 |
. . . . . 6
              
            
   |
46 | 44, 45 | bitri 184 |
. . . . 5
                  
   |
47 | | r2al 2496 |
. . . . 5
 

        
      

             |
48 | 41, 46, 47 | 3bitr4g 223 |
. . . 4
      


             |
49 | 2, 48 | syl 14 |
. . 3
           

             |
50 | 49 | pm5.32i 454 |
. 2
           
     

        
    |
51 | 1, 50 | bitri 184 |
1
    
     

        
    |