Step | Hyp | Ref
| Expression |
1 | | axinfndlem1 9061 |
. . . . . . 7
 
     
        |
2 | 1 | ax-gen 1680 |
. . . . . 6
                  |
3 | | nfnae 2163 |
. . . . . . . 8
   |
4 | | nfnae 2163 |
. . . . . . . 8
   |
5 | 3, 4 | nfan 2022 |
. . . . . . 7
       |
6 | | nfnae 2163 |
. . . . . . . . . 10
   |
7 | | nfnae 2163 |
. . . . . . . . . 10
   |
8 | 6, 7 | nfan 2022 |
. . . . . . . . 9
       |
9 | | nfcvd 2604 |
. . . . . . . . . 10
    
    |
10 | | nfcvf 2626 |
. . . . . . . . . . 11
 
    |
11 | 10 | adantl 472 |
. . . . . . . . . 10
    
    |
12 | 9, 11 | nfeld 2611 |
. . . . . . . . 9
    

  |
13 | 8, 12 | nfald 2045 |
. . . . . . . 8
    
  
  |
14 | | nfcvf 2626 |
. . . . . . . . . . . 12
 
    |
15 | 14 | adantr 471 |
. . . . . . . . . . 11
    
    |
16 | 9, 15 | nfeld 2611 |
. . . . . . . . . 10
    

  |
17 | | nfnae 2163 |
. . . . . . . . . . . 12
   |
18 | | nfnae 2163 |
. . . . . . . . . . . 12
   |
19 | 17, 18 | nfan 2022 |
. . . . . . . . . . 11
       |
20 | | nfnae 2163 |
. . . . . . . . . . . . . 14
   |
21 | | nfnae 2163 |
. . . . . . . . . . . . . 14
   |
22 | 20, 21 | nfan 2022 |
. . . . . . . . . . . . 13
       |
23 | 11, 15 | nfeld 2611 |
. . . . . . . . . . . . . 14
    
   |
24 | 12, 23 | nfand 2019 |
. . . . . . . . . . . . 13
    
      |
25 | 22, 24 | nfexd 2046 |
. . . . . . . . . . . 12
    
        |
26 | 16, 25 | nfimd 2011 |
. . . . . . . . . . 11
    
          |
27 | 19, 26 | nfald 2045 |
. . . . . . . . . 10
    
    
       |
28 | 16, 27 | nfand 2019 |
. . . . . . . . 9
    
              |
29 | 8, 28 | nfexd 2046 |
. . . . . . . 8
    
                |
30 | 13, 29 | nfimd 2011 |
. . . . . . 7
    
                   |
31 | | nfcvd 2604 |
. . . . . . . . . . . 12
    
    |
32 | | nfcvf2 2627 |
. . . . . . . . . . . . 13
 
    |
33 | 32 | adantr 471 |
. . . . . . . . . . . 12
    
    |
34 | 31, 33 | nfeqd 2610 |
. . . . . . . . . . 11
    

  |
35 | 8, 34 | nfan1 2021 |
. . . . . . . . . 10
    
 
  |
36 | | simpr 467 |
. . . . . . . . . . 11
      
  |
37 | 36 | eleq1d 2524 |
. . . . . . . . . 10
           |
38 | 35, 37 | albid 1974 |
. . . . . . . . 9
        

   |
39 | 36 | eleq1d 2524 |
. . . . . . . . . . 11
           |
40 | | nfcvd 2604 |
. . . . . . . . . . . . . . . . . 18
    
    |
41 | | nfcvf2 2627 |
. . . . . . . . . . . . . . . . . . 19
 
    |
42 | 41 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
    
    |
43 | 40, 42 | nfeqd 2610 |
. . . . . . . . . . . . . . . . 17
    

  |
44 | 22, 43 | nfan1 2021 |
. . . . . . . . . . . . . . . 16
    
 
  |
45 | 37 | anbi1d 716 |
. . . . . . . . . . . . . . . 16
         

    |
46 | 44, 45 | exbid 1975 |
. . . . . . . . . . . . . . 15
          
        |
47 | 39, 46 | imbi12d 326 |
. . . . . . . . . . . . . 14
        
    

        |
48 | 47 | ex 440 |
. . . . . . . . . . . . 13
    

      

         |
49 | 5, 26, 48 | cbvald 2129 |
. . . . . . . . . . . 12
    
   
    
           |
50 | 49 | adantr 471 |
. . . . . . . . . . 11
               
           |
51 | 39, 50 | anbi12d 722 |
. . . . . . . . . 10
                               |
52 | 35, 51 | exbid 1975 |
. . . . . . . . 9
             
     
               |
53 | 38, 52 | imbi12d 326 |
. . . . . . . 8
         
              
                |
54 | 53 | ex 440 |
. . . . . . 7
    

  
                                |
55 | 5, 30, 54 | cbvald 2129 |
. . . . . 6
    
    
                
     
          |
56 | 2, 55 | mpbii 216 |
. . . . 5
    
                   |
57 | 56 | 19.21bi 1958 |
. . . 4
    
 
     
         |
58 | 57 | ex 440 |
. . 3
 
   
                |
59 | | nd1 9043 |
. . . . 5
 
   |
60 | 59 | aecoms 2157 |
. . . 4
 
   |
61 | 60 | pm2.21d 110 |
. . 3
 
                 |
62 | | nd3 9045 |
. . . 4
 
   |
63 | 62 | pm2.21d 110 |
. . 3
 
                 |
64 | 58, 61, 63 | pm2.61ii 170 |
. 2
 
     
        |
65 | 64 | 19.35ri 1753 |
1
               |