Step | Hyp | Ref
| Expression |
1 | | axacndlem4 9035 |
. . . 4
                     
     |
2 | | nfnae 2152 |
. . . . . 6
   |
3 | | nfnae 2152 |
. . . . . 6
   |
4 | | nfnae 2152 |
. . . . . 6
   |
5 | 2, 3, 4 | nf3an 2013 |
. . . . 5
     
  |
6 | | nfnae 2152 |
. . . . . . 7
   |
7 | | nfnae 2152 |
. . . . . . 7
   |
8 | | nfnae 2152 |
. . . . . . 7
   |
9 | 6, 7, 8 | nf3an 2013 |
. . . . . 6
     
  |
10 | | nfnae 2152 |
. . . . . . . 8
   |
11 | | nfnae 2152 |
. . . . . . . 8
   |
12 | | nfnae 2152 |
. . . . . . . 8
   |
13 | 10, 11, 12 | nf3an 2013 |
. . . . . . 7
     
  |
14 | | nfcvd 2593 |
. . . . . . . . . . 11
          |
15 | | nfcvf 2615 |
. . . . . . . . . . . 12
 
    |
16 | 15 | 3ad2ant1 1029 |
. . . . . . . . . . 11
          |
17 | 14, 16 | nfeld 2600 |
. . . . . . . . . 10
         |
18 | | nfcvf 2615 |
. . . . . . . . . . . 12
 
    |
19 | 18 | 3ad2ant3 1031 |
. . . . . . . . . . 11
          |
20 | 16, 19 | nfeld 2600 |
. . . . . . . . . 10
         |
21 | 17, 20 | nfand 2008 |
. . . . . . . . 9
        
   |
22 | 5, 21 | nfald 2034 |
. . . . . . . 8
              |
23 | | nfnae 2152 |
. . . . . . . . . 10
   |
24 | | nfnae 2152 |
. . . . . . . . . 10
   |
25 | | nfnae 2152 |
. . . . . . . . . 10
   |
26 | 23, 24, 25 | nf3an 2013 |
. . . . . . . . 9
     
  |
27 | | nfv 1761 |
. . . . . . . . . 10
     
  |
28 | 14, 19 | nfeld 2600 |
. . . . . . . . . . . . . 14
         |
29 | | nfcvf 2615 |
. . . . . . . . . . . . . . . 16
 
    |
30 | 29 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . 15
          |
31 | 19, 30 | nfeld 2600 |
. . . . . . . . . . . . . 14
         |
32 | 28, 31 | nfand 2008 |
. . . . . . . . . . . . 13
        
   |
33 | 21, 32 | nfand 2008 |
. . . . . . . . . . . 12
          

    |
34 | 26, 33 | nfexd 2035 |
. . . . . . . . . . 11
             
    |
35 | 14, 19 | nfeqd 2599 |
. . . . . . . . . . 11
         |
36 | 34, 35 | nfbid 2016 |
. . . . . . . . . 10
            
 
 
   |
37 | 27, 36 | nfald 2034 |
. . . . . . . . 9
                
     |
38 | 26, 37 | nfexd 2035 |
. . . . . . . 8
                
 
 
   |
39 | 22, 38 | nfimd 2000 |
. . . . . . 7
                       
      |
40 | 13, 39 | nfald 2034 |
. . . . . 6
              
          
      |
41 | | nfcvd 2593 |
. . . . . . . . . 10
          |
42 | | nfcvf2 2616 |
. . . . . . . . . . 11
 
    |
43 | 42 | 3ad2ant1 1029 |
. . . . . . . . . 10
          |
44 | 41, 43 | nfeqd 2599 |
. . . . . . . . 9
         |
45 | 13, 44 | nfan1 2010 |
. . . . . . . 8
    
     |
46 | | nfcvd 2593 |
. . . . . . . . . . . 12
          |
47 | | nfcvf2 2616 |
. . . . . . . . . . . . 13
 
    |
48 | 47 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
          |
49 | 46, 48 | nfeqd 2599 |
. . . . . . . . . . 11
         |
50 | 5, 49 | nfan1 2010 |
. . . . . . . . . 10
    
     |
51 | | simpr 463 |
. . . . . . . . . . . 12
     

   |
52 | 51 | eleq1d 2513 |
. . . . . . . . . . 11
     

 
   |
53 | 52 | anbi1d 711 |
. . . . . . . . . 10
     

         |
54 | 50, 53 | albid 1963 |
. . . . . . . . 9
     

     
       |
55 | | nfcvd 2593 |
. . . . . . . . . . . . . . . . 17
          |
56 | | nfcvf2 2616 |
. . . . . . . . . . . . . . . . . 18
 
    |
57 | 56 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . 17
          |
58 | 55, 57 | nfeqd 2599 |
. . . . . . . . . . . . . . . 16
         |
59 | 26, 58 | nfan1 2010 |
. . . . . . . . . . . . . . 15
    
     |
60 | 51 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
     

 
   |
61 | 60 | anbi1d 711 |
. . . . . . . . . . . . . . . 16
     

  
      |
62 | 53, 61 | anbi12d 717 |
. . . . . . . . . . . . . . 15
     

     
     
     |
63 | 59, 62 | exbid 1964 |
. . . . . . . . . . . . . 14
     

       
     
 
     |
64 | 51 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
     

 
   |
65 | 63, 64 | bibi12d 323 |
. . . . . . . . . . . . 13
     

       

 

      
      |
66 | 65 | ex 436 |
. . . . . . . . . . . 12
      
       
         
       |
67 | 9, 36, 66 | cbvald 2118 |
. . . . . . . . . . 11
              

 

       

 
    |
68 | 26, 67 | exbid 1964 |
. . . . . . . . . 10
                 
            

 
    |
69 | 68 | adantr 467 |
. . . . . . . . 9
     

          
 
 

          
      |
70 | 54, 69 | imbi12d 322 |
. . . . . . . 8
     

     
          

 
 
               
       |
71 | 45, 70 | albid 1963 |
. . . . . . 7
     

        
          
   
     
          

 
     |
72 | 71 | ex 436 |
. . . . . 6
      
       
          
   
     
          

 
      |
73 | 9, 40, 72 | cbvald 2118 |
. . . . 5
               
          
   
        
          
       |
74 | 5, 73 | exbid 1964 |
. . . 4
                            
   
                     
       |
75 | 1, 74 | mpbii 215 |
. . 3
                
          
      |
76 | 75 | 3exp 1207 |
. 2
 
   
          
          
        |
77 | | axacndlem3 9034 |
. 2
 
          
          
      |
78 | | axacndlem1 9032 |
. . 3
 
          
          
      |
79 | 78 | aecoms 2146 |
. 2
 
          
          
      |
80 | | nfae 2150 |
. . . . 5
    |
81 | | en2lp 8118 |
. . . . . . . . 9

  |
82 | | elequ2 1901 |
. . . . . . . . . 10
 
   |
83 | 82 | anbi2d 710 |
. . . . . . . . 9
         |
84 | 81, 83 | mtbii 304 |
. . . . . . . 8
     |
85 | 84 | sps 1943 |
. . . . . . 7
 
    |
86 | 85 | pm2.21d 110 |
. . . . . 6
 
             
      |
87 | 86 | spsd 1945 |
. . . . 5
 
   
          

 
    |
88 | 80, 87 | alrimi 1955 |
. . . 4
 
                 
      |
89 | 88 | axc4i 1980 |
. . 3
 
       
          

 
    |
90 | | 19.8a 1935 |
. . 3
                    
                         
      |
91 | 89, 90 | syl 17 |
. 2
 
          
          
      |
92 | 76, 77, 79, 91 | pm2.61iii 171 |
1
                     
     |