Step | Hyp | Ref
| Expression |
1 | | vex 3060 |
. . . 4
 |
2 | | vex 3060 |
. . . 4
 |
3 | 1, 2 | eqvinop 4703 |
. . 3
                     |
4 | | 19.8a 1946 |
. . . . . . . . 9
      
                  |
5 | 4 | 19.23bi 1960 |
. . . . . . . 8
                
      |
6 | 5 | ex 440 |
. . . . . . 7
               
       |
7 | | vex 3060 |
. . . . . . . . 9
 |
8 | | vex 3060 |
. . . . . . . . 9
 |
9 | 7, 8 | opth 4693 |
. . . . . . . 8
       
   |
10 | 9 | anbi1i 706 |
. . . . . . . . . 10
        
 
    |
11 | 10 | 2exbii 1730 |
. . . . . . . . 9
            
          |
12 | | nfe1 1929 |
. . . . . . . . . . 11
           |
13 | | 19.8a 1946 |
. . . . . . . . . . . . . . . 16
  
      |
14 | 13 | anim2i 577 |
. . . . . . . . . . . . . . 15
  
          |
15 | 14 | anassrs 658 |
. . . . . . . . . . . . . 14
             |
16 | 15 | eximi 1718 |
. . . . . . . . . . . . 13
      
          |
17 | | biidd 245 |
. . . . . . . . . . . . . 14
 
                |
18 | 17 | drex1 2172 |
. . . . . . . . . . . . 13
 
                    |
19 | 16, 18 | syl5ib 227 |
. . . . . . . . . . . 12
 
                  |
20 | | anass 659 |
. . . . . . . . . . . . . . 15
      
    |
21 | 20 | exbii 1729 |
. . . . . . . . . . . . . 14
               |
22 | | 19.40 1742 |
. . . . . . . . . . . . . . 15
        
       |
23 | | nfeqf2 2146 |
. . . . . . . . . . . . . . . . 17
 
   |
24 | 23 | 19.9d 1979 |
. . . . . . . . . . . . . . . 16
 
 
   |
25 | 24 | anim1d 572 |
. . . . . . . . . . . . . . 15
 
  
              |
26 | 22, 25 | syl5 33 |
. . . . . . . . . . . . . 14
 
                |
27 | 21, 26 | syl5bi 225 |
. . . . . . . . . . . . 13
 
      

        |
28 | | 19.8a 1946 |
. . . . . . . . . . . . 13
      
          |
29 | 27, 28 | syl6 34 |
. . . . . . . . . . . 12
 
      
           |
30 | 19, 29 | pm2.61i 169 |
. . . . . . . . . . 11
      
          |
31 | 12, 30 | exlimi 2006 |
. . . . . . . . . 10
                   |
32 | | euequ1 2316 |
. . . . . . . . . . . . . 14

 |
33 | | equcom 1873 |
. . . . . . . . . . . . . . 15

  |
34 | 33 | eubii 2332 |
. . . . . . . . . . . . . 14
     |
35 | 32, 34 | mpbi 213 |
. . . . . . . . . . . . 13

 |
36 | | eupick 2376 |
. . . . . . . . . . . . 13
                    |
37 | 35, 36 | mpan 681 |
. . . . . . . . . . . 12
         
       |
38 | 37 | com12 32 |
. . . . . . . . . . 11
                 |
39 | | euequ1 2316 |
. . . . . . . . . . . . . 14
  |
40 | | equcom 1873 |
. . . . . . . . . . . . . . 15

  |
41 | 40 | eubii 2332 |
. . . . . . . . . . . . . 14
     |
42 | 39, 41 | mpbi 213 |
. . . . . . . . . . . . 13
  |
43 | | eupick 2376 |
. . . . . . . . . . . . 13
        
   |
44 | 42, 43 | mpan 681 |
. . . . . . . . . . . 12
         |
45 | 44 | com12 32 |
. . . . . . . . . . 11
         |
46 | 38, 45 | sylan9 667 |
. . . . . . . . . 10
 
         
   |
47 | 31, 46 | syl5 33 |
. . . . . . . . 9
 
         
   |
48 | 11, 47 | syl5bi 225 |
. . . . . . . 8
 
         
       |
49 | 9, 48 | sylbi 200 |
. . . . . . 7
               
       |
50 | 6, 49 | impbid 195 |
. . . . . 6
       
       
       |
51 | | eqeq1 2466 |
. . . . . . 7
                 |
52 | 51 | anbi1d 716 |
. . . . . . . . 9
         
           |
53 | 52 | 2exbidv 1781 |
. . . . . . . 8
             
       
       |
54 | 53 | bibi2d 324 |
. . . . . . 7
               
                 |
55 | 51, 54 | imbi12d 326 |
. . . . . 6
         
                  
       
         |
56 | 50, 55 | mpbiri 241 |
. . . . 5
        
             |
57 | 56 | adantr 471 |
. . . 4
    
  
                      |
58 | 57 | exlimivv 1789 |
. . 3
        
  
                      |
59 | 3, 58 | sylbi 200 |
. 2
        
             |
60 | 59 | pm2.43i 49 |
1
    
            |