Step | Hyp | Ref
| Expression |
1 | | axpowndlem3 9049 |
. . . . 5
               |
2 | 1 | ax-gen 1679 |
. . . 4
  
         
    |
3 | | nfnae 2162 |
. . . . . 6
   |
4 | | nfnae 2162 |
. . . . . 6
   |
5 | 3, 4 | nfan 2021 |
. . . . 5
       |
6 | | nfcvf 2625 |
. . . . . . . . 9
 
    |
7 | 6 | adantr 471 |
. . . . . . . 8
    
    |
8 | | nfcvd 2603 |
. . . . . . . 8
    
    |
9 | 7, 8 | nfeqd 2609 |
. . . . . . 7
    

  |
10 | 9 | nfnd 1994 |
. . . . . 6
    

  |
11 | | nfnae 2162 |
. . . . . . . 8
   |
12 | | nfnae 2162 |
. . . . . . . 8
   |
13 | 11, 12 | nfan 2021 |
. . . . . . 7
       |
14 | | nfv 1771 |
. . . . . . . 8
       |
15 | | nfnae 2162 |
. . . . . . . . . . . . 13
   |
16 | | nfnae 2162 |
. . . . . . . . . . . . 13
   |
17 | 15, 16 | nfan 2021 |
. . . . . . . . . . . 12
       |
18 | 7, 8 | nfeld 2610 |
. . . . . . . . . . . 12
    

  |
19 | 17, 18 | nfexd 2045 |
. . . . . . . . . . 11
    
  
  |
20 | | nfcvf 2625 |
. . . . . . . . . . . . . 14
 
    |
21 | 20 | adantl 472 |
. . . . . . . . . . . . 13
    
    |
22 | 7, 21 | nfeld 2610 |
. . . . . . . . . . . 12
    

  |
23 | 14, 22 | nfald 2044 |
. . . . . . . . . . 11
    
  
  |
24 | 19, 23 | nfimd 2010 |
. . . . . . . . . 10
    
    
   |
25 | 13, 24 | nfald 2044 |
. . . . . . . . 9
    
     
    |
26 | 8, 7 | nfeld 2610 |
. . . . . . . . 9
    

  |
27 | 25, 26 | nfimd 2010 |
. . . . . . . 8
    
      

    |
28 | 14, 27 | nfald 2044 |
. . . . . . 7
    
         
    |
29 | 13, 28 | nfexd 2045 |
. . . . . 6
    
                |
30 | 10, 29 | nfimd 2010 |
. . . . 5
    
  
         
     |
31 | | equequ2 1878 |
. . . . . . . . 9
 
   |
32 | 31 | notbid 300 |
. . . . . . . 8
 
   |
33 | 32 | adantl 472 |
. . . . . . 7
       
   |
34 | | nfcvd 2603 |
. . . . . . . . . . . . . . 15
    
    |
35 | | nfcvf2 2626 |
. . . . . . . . . . . . . . . 16
 
    |
36 | 35 | adantr 471 |
. . . . . . . . . . . . . . 15
    
    |
37 | 34, 36 | nfeqd 2609 |
. . . . . . . . . . . . . 14
    

  |
38 | 13, 37 | nfan1 2020 |
. . . . . . . . . . . . 13
    
 
  |
39 | | nfcvd 2603 |
. . . . . . . . . . . . . . . . 17
    
    |
40 | | nfcvf2 2626 |
. . . . . . . . . . . . . . . . . 18
 
    |
41 | 40 | adantl 472 |
. . . . . . . . . . . . . . . . 17
    
    |
42 | 39, 41 | nfeqd 2609 |
. . . . . . . . . . . . . . . 16
    

  |
43 | 17, 42 | nfan1 2020 |
. . . . . . . . . . . . . . 15
    
 
  |
44 | | elequ2 1911 |
. . . . . . . . . . . . . . . 16
 
   |
45 | 44 | adantl 472 |
. . . . . . . . . . . . . . 15
           |
46 | 43, 45 | exbid 1974 |
. . . . . . . . . . . . . 14
        

   |
47 | | biidd 245 |
. . . . . . . . . . . . . . . . 17
 
   |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
    


    |
49 | 5, 22, 48 | cbvald 2128 |
. . . . . . . . . . . . . . 15
    
 
    |
50 | 49 | adantr 471 |
. . . . . . . . . . . . . 14
        

   |
51 | 46, 50 | imbi12d 326 |
. . . . . . . . . . . . 13
         
   
     |
52 | 38, 51 | albid 1973 |
. . . . . . . . . . . 12
           

    
     |
53 | | elequ1 1904 |
. . . . . . . . . . . . 13
 
   |
54 | 53 | adantl 472 |
. . . . . . . . . . . 12
           |
55 | 52, 54 | imbi12d 326 |
. . . . . . . . . . 11
             
      

     |
56 | 55 | ex 440 |
. . . . . . . . . 10
    

        
    
 
     |
57 | 5, 27, 56 | cbvald 2128 |
. . . . . . . . 9
    
        
         
     |
58 | 13, 57 | exbid 1974 |
. . . . . . . 8
    
         
 

         
     |
59 | 58 | adantr 471 |
. . . . . . 7
                 
                 |
60 | 33, 59 | imbi12d 326 |
. . . . . 6
        
         
   
         
      |
61 | 60 | ex 440 |
. . . . 5
    

          

   
         
       |
62 | 5, 30, 61 | cbvald 2128 |
. . . 4
    
   
         
                      |
63 | 2, 62 | mpbii 216 |
. . 3
    
  
         
     |
64 | 63 | 19.21bi 1957 |
. 2
    

               |
65 | 64 | ex 440 |
1
 
  
         
      |