Step | Hyp | Ref
| Expression |
1 | | lo1bdd2.4 |
. . 3
         |
2 | | lo1bdd2.1 |
. . . 4

  |
3 | | lo1bdd2.3 |
. . . 4
 
   |
4 | | lo1bdd2.2 |
. . . 4
   |
5 | 2, 3, 4 | ello1mpt2 13102 |
. . 3
        
     

    |
6 | 1, 5 | mpbid 210 |
. 2
      
 
   |
7 | | elicopnf 11486 |
. . . . . . . . . . 11
    
     |
8 | 4, 7 | syl 16 |
. . . . . . . . . 10
          |
9 | 8 | biimpa 484 |
. . . . . . . . 9
 
   
    |
10 | | lo1bdd2.5 |
. . . . . . . . 9
 
  
  |
11 | 9, 10 | syldan 470 |
. . . . . . . 8
 
   
  |
12 | 11 | ad2antrr 725 |
. . . . . . 7
   
    
 
      |
13 | | simplrl 759 |
. . . . . . 7
   
    
 
   
  |
14 | 12, 13 | ifclda 3919 |
. . . . . 6
         
  
 
 
   |
15 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
          |
16 | 15 | sselda 3454 |
. . . . . . . . . . 11
   
   


  |
17 | 9 | simpld 459 |
. . . . . . . . . . . 12
 
   
  |
18 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
   
   


  |
19 | 16, 18 | ltnled 9622 |
. . . . . . . . . 10
   
   



   |
20 | | lo1bdd2.6 |
. . . . . . . . . . . . . . . . 17
     

 
  |
21 | 20 | expr 615 |
. . . . . . . . . . . . . . . 16
       
   |
22 | 21 | an32s 802 |
. . . . . . . . . . . . . . 15
      

   |
23 | 22 | ex 434 |
. . . . . . . . . . . . . 14
 
    
    |
24 | 9, 23 | syldan 470 |
. . . . . . . . . . . . 13
 
   

     |
25 | 24 | imp 429 |
. . . . . . . . . . . 12
        
   |
26 | 25 | adantlr 714 |
. . . . . . . . . . 11
   
   



   |
27 | | simplr 754 |
. . . . . . . . . . . . 13
   
   


  |
28 | 11 | ad2antrr 725 |
. . . . . . . . . . . . 13
   
   


  |
29 | | max2 11260 |
. . . . . . . . . . . . 13
 

 
 
   |
30 | 27, 28, 29 | syl2anc 661 |
. . . . . . . . . . . 12
   
   


       |
31 | | simpll 753 |
. . . . . . . . . . . . . 14
          |
32 | 31, 3 | sylan 471 |
. . . . . . . . . . . . 13
   
   


  |
33 | 11 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
          

  |
34 | | simpllr 758 |
. . . . . . . . . . . . . 14
          
   |
35 | 33, 34 | ifclda 3919 |
. . . . . . . . . . . . 13
   
   


 
 
   |
36 | | letr 9569 |
. . . . . . . . . . . . 13
 
 
 
   
 
 
 
        |
37 | 32, 28, 35, 36 | syl3anc 1219 |
. . . . . . . . . . . 12
   
   


    
           |
38 | 30, 37 | mpan2d 674 |
. . . . . . . . . . 11
   
   



        |
39 | 26, 38 | syld 44 |
. . . . . . . . . 10
   
   



        |
40 | 19, 39 | sylbird 235 |
. . . . . . . . 9
   
   


   
     |
41 | | max1 11258 |
. . . . . . . . . . 11
 

 
 
   |
42 | 27, 28, 41 | syl2anc 661 |
. . . . . . . . . 10
   
   


       |
43 | | letr 9569 |
. . . . . . . . . . 11
 
 
 
   
 
 
 
        |
44 | 32, 27, 35, 43 | syl3anc 1219 |
. . . . . . . . . 10
   
   


    
           |
45 | 42, 44 | mpan2d 674 |
. . . . . . . . 9
   
   



        |
46 | 40, 45 | jad 162 |
. . . . . . . 8
   
   


 
         |
47 | 46 | ralimdva 2824 |
. . . . . . 7
         

          |
48 | 47 | impr 619 |
. . . . . 6
         
  

       |
49 | | breq2 4394 |
. . . . . . . 8
      
        |
50 | 49 | ralbidv 2839 |
. . . . . . 7
       

        |
51 | 50 | rspcev 3169 |
. . . . . 6
    
         
   |
52 | 14, 48, 51 | syl2anc 661 |
. . . . 5
         
  
    |
53 | 52 | expr 615 |
. . . 4
         

      |
54 | 53 | rexlimdva 2937 |
. . 3
 
   
 



     |
55 | 54 | rexlimdva 2937 |
. 2
         
 
    |
56 | 6, 55 | mpd 15 |
1
     |