Step | Hyp | Ref
| Expression |
1 | | vex 3034 |
. . . . . . 7
 |
2 | | ax6e 2107 |
. . . . . . 7
  |
3 | 1, 2 | pm3.2i 462 |
. . . . . 6
 
  |
4 | | 19.42v 1842 |
. . . . . . 7
   

     |
5 | 4 | biimpri 211 |
. . . . . 6
   
      |
6 | 3, 5 | ax-mp 5 |
. . . . 5
     |
7 | | isset 3035 |
. . . . . . 7


  |
8 | 7 | anbi1i 709 |
. . . . . 6
 
      |
9 | 8 | exbii 1726 |
. . . . 5
   

       |
10 | 6, 9 | mpbi 213 |
. . . 4
      |
11 | | id 22 |
. . . . . 6
 

  |
12 | | hbnae 2166 |
. . . . . . 7
 
    |
13 | | hbn1 1933 |
. . . . . . . . . . . 12
 
    |
14 | | ax-5 1766 |
. . . . . . . . . . . . . . . 16
 
  |
15 | | ax-5 1766 |
. . . . . . . . . . . . . . . 16
    |
16 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
17 | | equequ1 1875 |
. . . . . . . . . . . . . . . . . 18
 
   |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
   |
19 | 18 | idiALT 36902 |
. . . . . . . . . . . . . . . 16
 
   |
20 | 14, 15, 19 | dvelimh 2185 |
. . . . . . . . . . . . . . 15
 


   |
21 | 11, 20 | syl 17 |
. . . . . . . . . . . . . 14
 


   |
22 | 21 | idiALT 36902 |
. . . . . . . . . . . . 13
 


   |
23 | 22 | alimi 1692 |
. . . . . . . . . . . 12
          |
24 | 13, 23 | syl 17 |
. . . . . . . . . . 11
 
       |
25 | 11, 24 | syl 17 |
. . . . . . . . . 10
 
       |
26 | | 19.41rg 36987 |
. . . . . . . . . 10
   

   
        |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
 
  

       |
28 | 27 | idiALT 36902 |
. . . . . . . 8
 
  

       |
29 | 28 | alimi 1692 |
. . . . . . 7
       
        |
30 | 12, 29 | syl 17 |
. . . . . 6
 
    
        |
31 | 11, 30 | syl 17 |
. . . . 5
 
    
        |
32 | | exim 1714 |
. . . . 5
      
         
          |
33 | 31, 32 | syl 17 |
. . . 4
 
    
          |
34 | | pm2.27 39 |
. . . 4
    
            
 
         |
35 | 10, 33, 34 | mpsyl 64 |
. . 3
 
        |
36 | | excomim 1946 |
. . 3
     
         |
37 | 35, 36 | syl 17 |
. 2
 
        |
38 | 37 | idiALT 36902 |
1
 
        |