Step | Hyp | Ref
| Expression |
1 | | breq1 4398 |
. . . . . . . 8
 
   |
2 | | eleq1 2537 |
. . . . . . . 8
 
   |
3 | 1, 2 | imbi12d 327 |
. . . . . . 7
  
      |
4 | 3 | imbi2d 323 |
. . . . . 6
    
  
 
       |
5 | | breq1 4398 |
. . . . . . . 8
 
   |
6 | | eleq1 2537 |
. . . . . . . 8
 
   |
7 | 5, 6 | imbi12d 327 |
. . . . . . 7
  
      |
8 | 7 | imbi2d 323 |
. . . . . 6
    
  
 
       |
9 | | r19.21v 2803 |
. . . . . . 7
 
     
 
 
     |
10 | | simpl1 1033 |
. . . . . . . . . . . . . . . 16
       |
11 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
12 | | onelss 5472 |
. . . . . . . . . . . . . . . . . 18
 
   |
13 | 12 | imp 436 |
. . . . . . . . . . . . . . . . 17
 

  |
14 | | ssdomg 7633 |
. . . . . . . . . . . . . . . . 17
 
   |
15 | 11, 13, 14 | mpsyl 64 |
. . . . . . . . . . . . . . . 16
 
   |
16 | 10, 15 | sylan 479 |
. . . . . . . . . . . . . . 15
    
 
  |
17 | | simplr 770 |
. . . . . . . . . . . . . . 15
    
 
  |
18 | | domtr 7640 |
. . . . . . . . . . . . . . 15
     |
19 | 16, 17, 18 | syl2anc 673 |
. . . . . . . . . . . . . 14
    
 
  |
20 | | pm2.27 39 |
. . . . . . . . . . . . . 14

      |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
    
 
      |
22 | 21 | ralimdva 2805 |
. . . . . . . . . . . 12
      
  
   |
23 | | dfss3 3408 |
. . . . . . . . . . . . 13


  |
24 | | domeng 7601 |
. . . . . . . . . . . . . . . 16
 
  
    |
25 | 24 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . 15
 
 
  
    |
26 | 25 | biimpa 492 |
. . . . . . . . . . . . . 14
       
   |
27 | | simpl2 1034 |
. . . . . . . . . . . . . . 15
       |
28 | | gruss 9239 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
29 | 28 | 3expia 1233 |
. . . . . . . . . . . . . . . . . . . 20
   
   |
30 | 29 | 3adant1 1048 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
31 | 30 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     
   |
32 | | ensym 7636 |
. . . . . . . . . . . . . . . . . . 19
   |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
     
   |
34 | 31, 33 | anim12d 572 |
. . . . . . . . . . . . . . . . 17
      
      |
35 | 34 | ancomsd 461 |
. . . . . . . . . . . . . . . 16
      
      |
36 | 35 | eximdv 1772 |
. . . . . . . . . . . . . . 15
         
  
    |
37 | | gruen 9255 |
. . . . . . . . . . . . . . . . . 18
    
  |
38 | 37 | 3com23 1237 |
. . . . . . . . . . . . . . . . 17
    
  |
39 | 38 | 3exp 1230 |
. . . . . . . . . . . . . . . 16

        |
40 | 39 | exlimdv 1787 |
. . . . . . . . . . . . . . 15

     
    |
41 | 27, 36, 40 | sylsyld 57 |
. . . . . . . . . . . . . 14
         

    |
42 | 26, 41 | mpd 15 |
. . . . . . . . . . . . 13
     
   |
43 | 23, 42 | syl5bir 226 |
. . . . . . . . . . . 12
      
   |
44 | 22, 43 | syld 44 |
. . . . . . . . . . 11
      
     |
45 | 44 | ex 441 |
. . . . . . . . . 10
 
   
      |
46 | 45 | com23 80 |
. . . . . . . . 9
 
  
       |
47 | 46 | 3expib 1234 |
. . . . . . . 8
     
 
      |
48 | 47 | a2d 28 |
. . . . . . 7
    

            |
49 | 9, 48 | syl5bi 225 |
. . . . . 6
  
  
            |
50 | 4, 8, 49 | tfis3 6703 |
. . . . 5
         |
51 | 50 | com3l 83 |
. . . 4
    
    |
52 | 51 | impr 631 |
. . 3
  
  
   |
53 | 52 | 3impia 1228 |
. 2
  

   |
54 | 53 | 3com23 1237 |
1
    
  |