Step | Hyp | Ref
| Expression |
1 | | euotd.4 |
. . . . . . . . . . . . 13
 

    |
2 | 1 | biimpa 487 |
. . . . . . . . . . . 12
 
     |
3 | | vex 3048 |
. . . . . . . . . . . . 13
 |
4 | | vex 3048 |
. . . . . . . . . . . . 13
 |
5 | | vex 3048 |
. . . . . . . . . . . . 13
 |
6 | 3, 4, 5 | otth 4684 |
. . . . . . . . . . . 12
    
        |
7 | 2, 6 | sylibr 216 |
. . . . . . . . . . 11
 
    
      |
8 | 7 | eqeq2d 2461 |
. . . . . . . . . 10
 
        
    |
9 | 8 | biimpd 211 |
. . . . . . . . 9
 
             |
10 | 9 | impancom 442 |
. . . . . . . 8
 
             |
11 | 10 | expimpd 608 |
. . . . . . 7
      
   
    |
12 | 11 | exlimdv 1779 |
. . . . . 6
         
  
    |
13 | 12 | exlimdvv 1780 |
. . . . 5
             
  
    |
14 | | euotd.3 |
. . . . . . . 8
   |
15 | | euotd.2 |
. . . . . . . . 9
   |
16 | | tru 1448 |
. . . . . . . . . . 11
 |
17 | | euotd.1 |
. . . . . . . . . . . 12
   |
18 | 15 | adantr 467 |
. . . . . . . . . . . . 13
 
   |
19 | 14 | ad2antrr 732 |
. . . . . . . . . . . . . 14
       |
20 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
 

      |
21 | 20, 6 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
 

     
      |
22 | 21 | eqcomd 2457 |
. . . . . . . . . . . . . . . . 17
 

            |
23 | 1 | biimpar 488 |
. . . . . . . . . . . . . . . . 17
 

    |
24 | 22, 23 | jca 535 |
. . . . . . . . . . . . . . . 16
 

      
       |
25 | | a1tru 1460 |
. . . . . . . . . . . . . . . 16
 

   |
26 | 24, 25 | 2thd 244 |
. . . . . . . . . . . . . . 15
 

      
    
   |
27 | 26 | 3anassrs 1232 |
. . . . . . . . . . . . . 14
   


      
    
  |
28 | 19, 27 | sbcied 3304 |
. . . . . . . . . . . . 13
      
 ![]. ].](_drbrack.gif)     
    
  |
29 | 18, 28 | sbcied 3304 |
. . . . . . . . . . . 12
 
  
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     
    
  |
30 | 17, 29 | sbcied 3304 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
    
   |
31 | 16, 30 | mpbiri 237 |
. . . . . . . . . 10
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     
       |
32 | 31 | spesbcd 3350 |
. . . . . . . . 9
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             |
33 | | nfcv 2592 |
. . . . . . . . . 10
   |
34 | | nfsbc1v 3287 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     
      |
35 | 34 | nfex 2031 |
. . . . . . . . . 10
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            |
36 | | sbceq1a 3278 |
. . . . . . . . . . 11
  
 ![]. ].](_drbrack.gif)     
    
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
    
    |
37 | 36 | exbidv 1768 |
. . . . . . . . . 10
      ![]. ].](_drbrack.gif)    
    
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
    
    |
38 | 33, 35, 37 | spcegf 3130 |
. . . . . . . . 9
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
    
     
 ![]. ].](_drbrack.gif)     
        |
39 | 15, 32, 38 | sylc 62 |
. . . . . . . 8
     
 ![]. ].](_drbrack.gif)     
       |
40 | | nfcv 2592 |
. . . . . . . . 9
   |
41 | | nfsbc1v 3287 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)     
      |
42 | 41 | nfex 2031 |
. . . . . . . . . 10
      ![]. ].](_drbrack.gif)            |
43 | 42 | nfex 2031 |
. . . . . . . . 9
      
 ![]. ].](_drbrack.gif)     
      |
44 | | sbceq1a 3278 |
. . . . . . . . . 10
      
    
  ![]. ].](_drbrack.gif)    
    
    |
45 | 44 | 2exbidv 1770 |
. . . . . . . . 9
               
      ![]. ].](_drbrack.gif)    
    
    |
46 | 40, 43, 45 | spcegf 3130 |
. . . . . . . 8
        ![]. ].](_drbrack.gif)                    
    
    |
47 | 14, 39, 46 | sylc 62 |
. . . . . . 7
          
    
   |
48 | | excom13 1930 |
. . . . . . 7
          
    
          
    
   |
49 | 47, 48 | sylib 200 |
. . . . . 6
          
    
   |
50 | | eqeq1 2455 |
. . . . . . . 8
    
    
  
        |
51 | 50 | anbi1d 711 |
. . . . . . 7
    
      
             |
52 | 51 | 3exbidv 1771 |
. . . . . 6
    
           
          
    
    |
53 | 49, 52 | syl5ibrcom 226 |
. . . . 5
                
    |
54 | 13, 53 | impbid 194 |
. . . 4
             
       |
55 | 54 | alrimiv 1773 |
. . 3
              
        |
56 | | otex 4665 |
. . . 4
  
  |
57 | | eqeq2 2462 |
. . . . . 6
    

       |
58 | 57 | bibi2d 320 |
. . . . 5
    
            
 
            
        |
59 | 58 | albidv 1767 |
. . . 4
    
               

              
        |
60 | 56, 59 | spcev 3141 |
. . 3
               
                     
   |
61 | 55, 60 | syl 17 |
. 2
                 
   |
62 | | df-eu 2303 |
. 2
              
                
   |
63 | 61, 62 | sylibr 216 |
1
                 |