Proof of Theorem ax6e2ndeqALT
Step | Hyp | Ref
| Expression |
1 | | ax6e2nd 36968 |
. . 3
 
        |
2 | | ax6e2eq 36967 |
. . . 4
 
          |
3 | 1 | a1d 26 |
. . . 4
 

         |
4 | | exmid 421 |
. . . 4
 
   |
5 | | jao 519 |
. . . . 5
  

          

          
              |
6 | 5 | 3imp 1208 |
. . . 4
         
    

         
             |
7 | 2, 3, 4, 6 | mp3an 1373 |
. . 3
         |
8 | 1, 7 | jaoi 385 |
. 2
        
   |
9 | | hbnae 2161 |
. . . . . . . . 9
 
    |
10 | 9 | eximi 1717 |
. . . . . . . 8
  
      |
11 | | nfa1 1989 |
. . . . . . . . 9
   
 |
12 | 11 | 19.9 1980 |
. . . . . . . 8
      
  |
13 | 10, 12 | sylib 201 |
. . . . . . 7
  
 
  |
14 | | sp 1947 |
. . . . . . 7
      |
15 | 13, 14 | syl 17 |
. . . . . 6
  
   |
16 | | excom 1937 |
. . . . . . 7
     
     
   |
17 | | nfa1 1989 |
. . . . . . . . . . . 12
  
 |
18 | 17 | nfn 1993 |
. . . . . . . . . . 11
   |
19 | 18 | 19.9 1980 |
. . . . . . . . . 10
  

  |
20 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
21 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
  
  
   |
22 | | simpl 463 |
. . . . . . . . . . . . . . . . 17
 
   |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
  
    |
24 | | pm13.181 2717 |
. . . . . . . . . . . . . . . . 17
     |
25 | 24 | ancoms 459 |
. . . . . . . . . . . . . . . 16
 
   |
26 | 20, 23, 25 | syl2an2r 847 |
. . . . . . . . . . . . . . 15
  
    |
27 | | simpr 467 |
. . . . . . . . . . . . . . . 16
 
   |
28 | 21, 27 | syl 17 |
. . . . . . . . . . . . . . 15
  
    |
29 | | neeq2 2698 |
. . . . . . . . . . . . . . . 16
 
   |
30 | 29 | biimparc 494 |
. . . . . . . . . . . . . . 15
 
   |
31 | 26, 28, 30 | syl2anc 671 |
. . . . . . . . . . . . . 14
  
    |
32 | | df-ne 2634 |
. . . . . . . . . . . . . . . 16

  |
33 | 32 | bicomi 207 |
. . . . . . . . . . . . . . 15

  |
34 | | sp 1947 |
. . . . . . . . . . . . . . . 16
 
  |
35 | 34 | con3i 142 |
. . . . . . . . . . . . . . 15
    |
36 | 33, 35 | sylbir 218 |
. . . . . . . . . . . . . 14
    |
37 | 31, 36 | syl 17 |
. . . . . . . . . . . . 13
  
     |
38 | 37 | ex 440 |
. . . . . . . . . . . 12
   

   |
39 | 38 | alrimiv 1783 |
. . . . . . . . . . 11
          |
40 | | exim 1716 |
. . . . . . . . . . 11
                  |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
           |
42 | | imbi2 330 |
. . . . . . . . . . 11
   
      
  
     

    |
43 | 42 | biimpa 491 |
. . . . . . . . . 10
                   
     |
44 | 19, 41, 43 | sylancr 674 |
. . . . . . . . 9
          |
45 | 44 | alrimiv 1783 |
. . . . . . . 8
      
     |
46 | | exim 1716 |
. . . . . . . 8
       

             |
47 | 45, 46 | syl 17 |
. . . . . . 7
      
  
   |
48 | | imbi1 329 |
. . . . . . . 8
                         
       

    |
49 | 48 | biimpar 492 |
. . . . . . 7
        
             
                |
50 | 16, 47, 49 | sylancr 674 |
. . . . . 6
      
  
   |
51 | | pm3.34 594 |
. . . . . 6
    

                       |
52 | 15, 50, 51 | sylancr 674 |
. . . . 5
      
     |
53 | | orc 391 |
. . . . . 6
 
     |
54 | 53 | imim2i 16 |
. . . . 5
       

              |
55 | 52, 54 | syl 17 |
. . . 4
      
  
    |
56 | 55 | idiALT 36875 |
. . 3
      
  
    |
57 | | id 22 |
. . . . . 6
   |
58 | | ax-1 6 |
. . . . . 6
      
    |
59 | 57, 58 | syl 17 |
. . . . 5
      
    |
60 | | olc 390 |
. . . . . 6
      |
61 | 60 | imim2i 16 |
. . . . 5
       
      
  
    |
62 | 59, 61 | syl 17 |
. . . 4
      
  
    |
63 | 62 | idiALT 36875 |
. . 3
      
  
    |
64 | | exmidne 2644 |
. . 3
   |
65 | | jao 519 |
. . . 4
                     
  
     
        
      |
66 | 65 | 3imp21 1227 |
. . 3
               
        
     
        
    |
67 | 56, 63, 64, 66 | mp3an 1373 |
. 2
     
  
   |
68 | 8, 67 | impbii 192 |
1
   
        |