Step | Hyp | Ref
| Expression |
1 | | df-we 4813 |
. 2


   |
2 | | df-so 4774 |
. . . 4




  
      |
3 | | simpr 467 |
. . . . 5
   
      


  
     |
4 | | ax-1 6 |
. . . . . . . . . . . . . . 15
         
     |
5 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
  
                  |
6 | | fr2nr 4830 |
. . . . . . . . . . . . . . . . 17
  
          |
7 | 6 | 3adantr3 1175 |
. . . . . . . . . . . . . . . 16
  
          |
8 | | breq2 4419 |
. . . . . . . . . . . . . . . . . 18
   
     |
9 | 8 | anbi2d 715 |
. . . . . . . . . . . . . . . . 17
                 |
10 | 9 | notbid 300 |
. . . . . . . . . . . . . . . 16
       
         |
11 | 7, 10 | syl5ibcom 228 |
. . . . . . . . . . . . . . 15
  
            |
12 | | pm2.21 112 |
. . . . . . . . . . . . . . 15
      
            |
13 | 11, 12 | syl6 34 |
. . . . . . . . . . . . . 14
  
                |
14 | | fr3nr 6632 |
. . . . . . . . . . . . . . . . 17
  
            |
15 | | df-3an 993 |
. . . . . . . . . . . . . . . . . . 19
        
            |
16 | 15 | biimpri 211 |
. . . . . . . . . . . . . . . . . 18
                     |
17 | 16 | ancoms 459 |
. . . . . . . . . . . . . . . . 17
                     |
18 | 14, 17 | nsyl 126 |
. . . . . . . . . . . . . . . 16
  
              |
19 | 18 | pm2.21d 110 |
. . . . . . . . . . . . . . 15
  
                  |
20 | 19 | expd 442 |
. . . . . . . . . . . . . 14
  
                  |
21 | 5, 13, 20 | 3jaod 1341 |
. . . . . . . . . . . . 13
  
        
             |
22 | | frirr 4829 |
. . . . . . . . . . . . . 14
 
     |
23 | 22 | 3ad2antr1 1179 |
. . . . . . . . . . . . 13
  
      |
24 | 21, 23 | jctild 550 |
. . . . . . . . . . . 12
  
        
         
       |
25 | 24 | ex 440 |
. . . . . . . . . . 11
  

         
      
        |
26 | 25 | a2d 29 |
. . . . . . . . . 10
           
 
                   |
27 | 26 | alimdv 1773 |
. . . . . . . . 9
     
       
                       |
28 | 27 | 2alimdv 1775 |
. . . . . . . 8
         
       
       

         
        |
29 | | r3al 2779 |
. . . . . . . 8
 


             
          |
30 | | r3al 2779 |
. . . . . . . 8
 


                     
                  |
31 | 28, 29, 30 | 3imtr4g 278 |
. . . . . . 7
  


     



         
       |
32 | | ralidm 3884 |
. . . . . . . . 9
 

      
        |
33 | | breq2 4419 |
. . . . . . . . . . . 12
   
     |
34 | | equequ2 1878 |
. . . . . . . . . . . 12
 
   |
35 | | breq1 4418 |
. . . . . . . . . . . 12
   
     |
36 | 33, 34, 35 | 3orbi123d 1347 |
. . . . . . . . . . 11
                 |
37 | 36 | cbvralv 3030 |
. . . . . . . . . 10
 
      
        |
38 | 37 | ralbii 2830 |
. . . . . . . . 9
 

      

        |
39 | 32, 38 | bitr3i 259 |
. . . . . . . 8
 
      

        |
40 | 39 | ralbii 2830 |
. . . . . . 7
 

      


        |
41 | | df-po 4773 |
. . . . . . 7




         
      |
42 | 31, 40, 41 | 3imtr4g 278 |
. . . . . 6
  

     
   |
43 | 42 | ancrd 561 |
. . . . 5
  

     



  
       |
44 | 3, 43 | impbid2 209 |
. . . 4
    
      


  
      |
45 | 2, 44 | syl5bb 265 |
. . 3
 


  
      |
46 | 45 | pm5.32i 647 |
. 2
 
   
         |
47 | 1, 46 | bitri 257 |
1




  
      |