Step | Hyp | Ref
| Expression |
1 | | axpowndlem4 9043 |
. 2
 
  
         
      |
2 | | axpowndlem1 9040 |
. . 3
 

         
     |
3 | 2 | aecoms 2161 |
. 2
 

         
     |
4 | 2 | a1d 25 |
. . 3
 
  
        

      |
5 | | nfnae 2167 |
. . . . . . . 8
   |
6 | | nfae 2165 |
. . . . . . . 8
    |
7 | 5, 6 | nfan 2031 |
. . . . . . 7
   
   |
8 | | el 4583 |
. . . . . . . . . . . . 13

 |
9 | | nfcvf2 2636 |
. . . . . . . . . . . . . . 15
 
    |
10 | | nfcvd 2613 |
. . . . . . . . . . . . . . 15
 
    |
11 | 9, 10 | nfeld 2620 |
. . . . . . . . . . . . . 14
 

  |
12 | | elequ2 1918 |
. . . . . . . . . . . . . . 15
 
   |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . 14
 


    |
14 | 5, 11, 13 | cbvexd 2132 |
. . . . . . . . . . . . 13
 
 
    |
15 | 8, 14 | mpbii 216 |
. . . . . . . . . . . 12
 

  |
16 | | 19.8a 1955 |
. . . . . . . . . . . 12
    
  |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
 
  
  |
18 | | df-ex 1672 |
. . . . . . . . . . 11
   
    |
19 | 17, 18 | sylib 201 |
. . . . . . . . . 10
 
    |
20 | 19 | adantr 472 |
. . . . . . . . 9
   

    |
21 | | biidd 245 |
. . . . . . . . . . . . . 14
 

   |
22 | 21 | dral1 2174 |
. . . . . . . . . . . . 13
 
 

   |
23 | | alnex 1673 |
. . . . . . . . . . . . 13
     |
24 | | alnex 1673 |
. . . . . . . . . . . . 13
     |
25 | 22, 23, 24 | 3bitr3g 295 |
. . . . . . . . . . . 12
 
 

   |
26 | | nd2 9031 |
. . . . . . . . . . . . 13
 
   |
27 | | mtt 346 |
. . . . . . . . . . . . 13
 
    
    |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
 
 
 
     |
29 | 25, 28 | bitrd 261 |
. . . . . . . . . . 11
 
 
 
     |
30 | 29 | dral2 2173 |
. . . . . . . . . 10
 
      
     |
31 | 30 | adantl 473 |
. . . . . . . . 9
   

  
    
    |
32 | 20, 31 | mtbid 307 |
. . . . . . . 8
   

    
   |
33 | 32 | pm2.21d 109 |
. . . . . . 7
   

    
 
   |
34 | 7, 33 | alrimi 1975 |
. . . . . 6
   

      

    |
35 | | 19.8a 1955 |
. . . . . 6
        
          

    |
36 | 34, 35 | syl 17 |
. . . . 5
   

         
    |
37 | 36 | a1d 25 |
. . . 4
   


               |
38 | 37 | ex 441 |
. . 3
 
 

         
      |
39 | 4, 38 | pm2.61i 169 |
. 2
 

         
     |
40 | 1, 3, 39 | pm2.61ii 170 |
1
               |