Proof of Theorem cdlemefrs29bpre0
Step | Hyp | Ref
| Expression |
1 | | df-ral 2761 |
. . 3
 
             
     
     

       |
2 | | anass 661 |
. . . . . . 7
       
               |
3 | 2 | imbi1i 332 |
. . . . . 6
    
  
     
  
                  |
4 | | impexp 453 |
. . . . . 6
    
  
     
  
  
               |
5 | | impexp 453 |
. . . . . 6
                 
                 |
6 | 3, 4, 5 | 3bitr3ri 284 |
. . . . 5
    
     

    
  
               |
7 | | simpl11 1105 |
. . . . . . . . . . . 12
      
    
        
    |
8 | | simpl2r 1084 |
. . . . . . . . . . . 12
      
    
        

   |
9 | | cdlemefrs27.l |
. . . . . . . . . . . . 13
     |
10 | | cdlemefrs27.m |
. . . . . . . . . . . . 13
     |
11 | | eqid 2471 |
. . . . . . . . . . . . 13
         |
12 | | cdlemefrs27.a |
. . . . . . . . . . . . 13
     |
13 | | cdlemefrs27.h |
. . . . . . . . . . . . 13
     |
14 | 9, 10, 11, 12, 13 | lhpmat 33666 |
. . . . . . . . . . . 12
               |
15 | 7, 8, 14 | syl2anc 673 |
. . . . . . . . . . 11
      
    
        
        |
16 | 15 | oveq2d 6324 |
. . . . . . . . . 10
      
    
        
            |
17 | | simp11l 1141 |
. . . . . . . . . . . . 13
     
    
      |
18 | | hlol 32998 |
. . . . . . . . . . . . 13
   |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
     
    
      |
20 | 19 | adantr 472 |
. . . . . . . . . . 11
      
    
        
  |
21 | | simprl 772 |
. . . . . . . . . . . 12
      
    
        
  |
22 | | cdlemefrs27.b |
. . . . . . . . . . . . 13
     |
23 | 22, 12 | atbase 32926 |
. . . . . . . . . . . 12
   |
24 | 21, 23 | syl 17 |
. . . . . . . . . . 11
      
    
        
  |
25 | | cdlemefrs27.j |
. . . . . . . . . . . 12
     |
26 | 22, 25, 11 | olj01 32862 |
. . . . . . . . . . 11
 
         |
27 | 20, 24, 26 | syl2anc 673 |
. . . . . . . . . 10
      
    
        
        |
28 | 16, 27 | eqtrd 2505 |
. . . . . . . . 9
      
    
        
      |
29 | 28 | eqeq1d 2473 |
. . . . . . . 8
      
    
        
 
      |
30 | 15 | oveq2d 6324 |
. . . . . . . . . 10
      
    
        
            |
31 | | simpl1 1033 |
. . . . . . . . . . . 12
      
    
        
 
 
      |
32 | | simpl2l 1083 |
. . . . . . . . . . . 12
      
    
        
  |
33 | | simprr 774 |
. . . . . . . . . . . 12
      
    
        
    |
34 | | cdlemefrs27.nb |
. . . . . . . . . . . 12
     
     
  
  |
35 | 31, 32, 21, 33, 34 | syl112anc 1296 |
. . . . . . . . . . 11
      
    
        
  |
36 | 22, 25, 11 | olj01 32862 |
. . . . . . . . . . 11
 
         |
37 | 20, 35, 36 | syl2anc 673 |
. . . . . . . . . 10
      
    
        
        |
38 | 30, 37 | eqtrd 2505 |
. . . . . . . . 9
      
    
        
      |
39 | 38 | eqeq2d 2481 |
. . . . . . . 8
      
    
        
  
     |
40 | 29, 39 | imbi12d 327 |
. . . . . . 7
      
    
        
       
  

    |
41 | 40 | pm5.74da 701 |
. . . . . 6
     
    
       
        
   
  
  
     |
42 | | impexp 453 |
. . . . . . 7
    
   
  
  
    |
43 | | eqcom 2478 |
. . . . . . . . 9

  |
44 | 43 | imbi2i 319 |
. . . . . . . 8
       |
45 | | simp2rl 1099 |
. . . . . . . . . . 11
     
    
      |
46 | | simp2rr 1100 |
. . . . . . . . . . 11
     
    
      |
47 | | simp3 1032 |
. . . . . . . . . . 11
     
    
      |
48 | | eleq1 2537 |
. . . . . . . . . . . . 13
 
   |
49 | | breq1 4398 |
. . . . . . . . . . . . . . 15
 
   |
50 | 49 | notbid 301 |
. . . . . . . . . . . . . 14
 
   |
51 | | cdlemefrs27.eq |
. . . . . . . . . . . . . 14
     |
52 | 50, 51 | anbi12d 725 |
. . . . . . . . . . . . 13
   
     |
53 | 48, 52 | anbi12d 725 |
. . . . . . . . . . . 12
             |
54 | 53 | biimprcd 233 |
. . . . . . . . . . 11
  
  


     |
55 | 45, 46, 47, 54 | syl12anc 1290 |
. . . . . . . . . 10
     
    
      
     |
56 | 55 | pm4.71rd 647 |
. . . . . . . . 9
     
    
       
      |
57 | 56 | imbi1d 324 |
. . . . . . . 8
     
    
     

      
    |
58 | 44, 57 | syl5rbbr 268 |
. . . . . . 7
     
    
        
  


    |
59 | 42, 58 | syl5bbr 267 |
. . . . . 6
     
    
       
     
    |
60 | 41, 59 | bitrd 261 |
. . . . 5
     
    
       
        
   

    |
61 | 6, 60 | syl5bb 265 |
. . . 4
     
    
     
                    |
62 | 61 | albidv 1775 |
. . 3
     
    
          
     

    
       |
63 | 1, 62 | syl5bb 265 |
. 2
     
    
              

           |
64 | | nfcv 2612 |
. . . . 5
   |
65 | 64 | csbiebg 3372 |
. . . 4
    

  ![]_ ]_](_urbrack.gif)    |
66 | 45, 65 | syl 17 |
. . 3
     
    
       
   ![]_ ]_](_urbrack.gif)
   |
67 | | eqcom 2478 |
. . 3
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
68 | 66, 67 | syl6bb 269 |
. 2
     
    
       
   ![]_ ]_](_urbrack.gif)    |
69 | 63, 68 | bitrd 261 |
1
     
    
              

      ![]_ ]_](_urbrack.gif)    |