Proof of Theorem reusv3
Step | Hyp | Ref
| Expression |
1 | | reusv3.1 |
. . . . 5
     |
2 | | reusv3.2 |
. . . . . 6
   |
3 | 2 | eleq1d 2181 |
. . . . 5
 
   |
4 | 1, 3 | anbi12d 462 |
. . . 4
  

     |
5 | 4 | cbvrexv 2627 |
. . 3
  


    |
6 | | nfra2xy 2447 |
. . . . 5
   
  
  |
7 | | nfv 1489 |
. . . . 5
   

  |
8 | 6, 7 | nfim 1532 |
. . . 4
         

    |
9 | | risset 2435 |
. . . . . 6


  |
10 | | ralcom 2566 |
. . . . . . . . . . . . . 14
 

 
  

  
   |
11 | | impexp 261 |
. . . . . . . . . . . . . . . . . 18
      
    |
12 | | bi2.04 247 |
. . . . . . . . . . . . . . . . . 18
           |
13 | 11, 12 | bitri 183 |
. . . . . . . . . . . . . . . . 17
           |
14 | 13 | ralbii 2413 |
. . . . . . . . . . . . . . . 16
 
 
  

     |
15 | | r19.21v 2481 |
. . . . . . . . . . . . . . . 16
 
     
     |
16 | 14, 15 | bitri 183 |
. . . . . . . . . . . . . . 15
 
 
   
     |
17 | 16 | ralbii 2413 |
. . . . . . . . . . . . . 14
 

 
  


     |
18 | 10, 17 | bitri 183 |
. . . . . . . . . . . . 13
 

 
  


     |
19 | | rsp 2452 |
. . . . . . . . . . . . 13
 
  
    
      |
20 | 18, 19 | sylbi 120 |
. . . . . . . . . . . 12
 

 
  
  
     |
21 | 20 | com3l 81 |
. . . . . . . . . . 11
   

  
  
     |
22 | 21 | imp31 254 |
. . . . . . . . . 10
    

 
  

    |
23 | | eqeq1 2119 |
. . . . . . . . . . . . 13
 
   |
24 | | eqcom 2115 |
. . . . . . . . . . . . 13

  |
25 | 23, 24 | syl6bb 195 |
. . . . . . . . . . . 12
 
   |
26 | 25 | imbi2d 229 |
. . . . . . . . . . 11
  

     |
27 | 26 | ralbidv 2409 |
. . . . . . . . . 10
  



     |
28 | 22, 27 | syl5ibrcom 156 |
. . . . . . . . 9
    

 
  


     |
29 | 28 | reximdv 2505 |
. . . . . . . 8
    

 
  
 


     |
30 | 29 | ex 114 |
. . . . . . 7
  
 

 
   
 

     |
31 | 30 | com23 78 |
. . . . . 6
  
   

  
 

      |
32 | 9, 31 | syl5bi 151 |
. . . . 5
  
  

  
 

      |
33 | 32 | expimpd 358 |
. . . 4
     

  
 

      |
34 | 8, 33 | rexlimi 2514 |
. . 3
     

  
 

     |
35 | 5, 34 | sylbi 120 |
. 2
  
  

  
 

     |
36 | 1, 2 | reusv3i 4338 |
. 2
  
 


  
   |
37 | 35, 36 | impbid1 141 |
1
  
  

  



     |