Step | Hyp | Ref
| Expression |
1 | | eqidd 2452 |
. . . . 5

  |
2 | 1 | ancli 554 |
. . . 4
     |
3 | | unirep.1 |
. . . . . 6
     |
4 | | unirep.2 |
. . . . . . 7
   |
5 | 4 | eqeq2d 2461 |
. . . . . 6
 
   |
6 | 3, 5 | anbi12d 717 |
. . . . 5
  

     |
7 | 6 | rspcev 3150 |
. . . 4
  
  
    |
8 | 2, 7 | sylan2 477 |
. . 3
  

    |
9 | 8 | adantl 468 |
. 2
   
  
 
  
    |
10 | | nfcvd 2593 |
. . . . . 6
     |
11 | 10, 4 | csbiegf 3387 |
. . . . 5
   ![]_ ]_](_urbrack.gif)   |
12 | | unirep.5 |
. . . . . 6
 |
13 | 12 | csbex 4538 |
. . . . 5
  ![]_ ]_](_urbrack.gif)  |
14 | 11, 13 | syl6eqelr 2538 |
. . . 4
   |
15 | 14 | ad2antrl 734 |
. . 3
   
  
 
    |
16 | | eqeq1 2455 |
. . . . . . . . . . 11
 
   |
17 | 16 | anbi2d 710 |
. . . . . . . . . 10
  

     |
18 | 17 | rexbidv 2901 |
. . . . . . . . 9
  
 

     |
19 | 18 | spcegv 3135 |
. . . . . . . 8
  
    
     |
20 | 14, 19 | syl 17 |
. . . . . . 7
  
    
     |
21 | 20 | adantr 467 |
. . . . . 6
  
  
   
     |
22 | 8, 21 | mpd 15 |
. . . . 5
  
  
    |
23 | 22 | adantl 468 |
. . . 4
   
  
 
    
    |
24 | | r19.29 2925 |
. . . . . . . 8
   
  
 
   
 
 
  
    |
25 | | r19.29 2925 |
. . . . . . . . . . . 12
     
 
   
  
  
    |
26 | | an4 833 |
. . . . . . . . . . . . . . . . 17
      
   
    |
27 | | pm3.35 591 |
. . . . . . . . . . . . . . . . . . . 20
        
  |
28 | | eqeq12 2464 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
29 | 27, 28 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . 19
               |
30 | 29 | ancoms 455 |
. . . . . . . . . . . . . . . . . 18
    
          |
31 | 30 | expimpd 608 |
. . . . . . . . . . . . . . . . 17
    
  
       |
32 | 26, 31 | syl5bi 221 |
. . . . . . . . . . . . . . . 16
    
  
       |
33 | 32 | ancomsd 456 |
. . . . . . . . . . . . . . 15
    
          |
34 | 33 | expdimp 439 |
. . . . . . . . . . . . . 14
    
     
    |
35 | 34 | rexlimivw 2876 |
. . . . . . . . . . . . 13
     
     
    |
36 | 35 | imp 431 |
. . . . . . . . . . . 12
                |
37 | 25, 36 | sylan 474 |
. . . . . . . . . . 11
        
        |
38 | 37 | an32s 813 |
. . . . . . . . . 10
           
     |
39 | 38 | ex 436 |
. . . . . . . . 9
     
     

    |
40 | 39 | rexlimivw 2876 |
. . . . . . . 8
      
     

    |
41 | 24, 40 | syl 17 |
. . . . . . 7
   
  
 
    

    |
42 | 41 | expimpd 608 |
. . . . . 6
 

 
     
 
      |
43 | 42 | adantr 467 |
. . . . 5
   
  
 
     
  
 
   |
44 | 43 | alrimivv 1774 |
. . . 4
   
  
 
         
 
      |
45 | | eqeq1 2455 |
. . . . . . . 8
 
   |
46 | 45 | anbi2d 710 |
. . . . . . 7
  

     |
47 | 46 | rexbidv 2901 |
. . . . . 6
  
 

     |
48 | | unirep.3 |
. . . . . . . 8
     |
49 | | unirep.4 |
. . . . . . . . 9
   |
50 | 49 | eqeq2d 2461 |
. . . . . . . 8
 
   |
51 | 48, 50 | anbi12d 717 |
. . . . . . 7
  

     |
52 | 51 | cbvrexv 3020 |
. . . . . 6
  


    |
53 | 47, 52 | syl6bb 265 |
. . . . 5
  
 

     |
54 | 53 | eu4 2347 |
. . . 4
    
    
         
 
       |
55 | 23, 44, 54 | sylanbrc 670 |
. . 3
   
  
 
         |
56 | 18 | iota2 5572 |
. . 3
     
 
 
     
      |
57 | 15, 55, 56 | syl2anc 667 |
. 2
   
  
 
   
 
          |
58 | 9, 57 | mpbid 214 |
1
   
  
 
      
    |