Step | Hyp | Ref
| Expression |
1 | | simplr 528 |
. . . . . . 7
  EXMID TAp


TAp   |
2 | | simpr 110 |
. . . . . . 7
  EXMID TAp


  |
3 | | dftap2 7250 |
. . . . . . . . . 10
 TAp  

 
  

        


          

  
     |
4 | 3 | biimpi 120 |
. . . . . . . . 9
 TAp
  
 
  

        


          

  
     |
5 | 4 | simp1d 1009 |
. . . . . . . 8
 TAp
    |
6 | 5 | sseld 3155 |
. . . . . . 7
 TAp

     |
7 | 1, 2, 6 | sylc 62 |
. . . . . 6
  EXMID TAp



   |
8 | | 1st2nd2 6176 |
. . . . . 6
                |
9 | 7, 8 | syl 14 |
. . . . 5
  EXMID TAp


             |
10 | | xp1st 6166 |
. . . . . . . 8
         |
11 | 7, 10 | syl 14 |
. . . . . . 7
  EXMID TAp


      |
12 | | xp2nd 6167 |
. . . . . . . 8
         |
13 | 7, 12 | syl 14 |
. . . . . . 7
  EXMID TAp


      |
14 | 9, 2 | eqeltrrd 2255 |
. . . . . . . . . 10
  EXMID TAp


             |
15 | 14 | adantr 276 |
. . . . . . . . 9
   EXMID TAp


        
             |
16 | | simpr 110 |
. . . . . . . . . . 11
   EXMID TAp


        
          |
17 | 16 | opeq2d 3786 |
. . . . . . . . . 10
   EXMID TAp


        
          
             |
18 | | id 19 |
. . . . . . . . . . . . . 14
    
      |
19 | 18, 18 | breq12d 4017 |
. . . . . . . . . . . . 13
    
  
             |
20 | 19 | notbid 667 |
. . . . . . . . . . . 12
    
  
             |
21 | 4 | simp2d 1010 |
. . . . . . . . . . . . . 14
 TAp
 
  

         |
22 | 21 | simpld 112 |
. . . . . . . . . . . . 13
 TAp

    |
23 | 22 | ad3antlr 493 |
. . . . . . . . . . . 12
   EXMID TAp


        

    |
24 | 11 | adantr 276 |
. . . . . . . . . . . 12
   EXMID TAp


        
      |
25 | 20, 23, 24 | rspcdva 2847 |
. . . . . . . . . . 11
   EXMID TAp


        
            |
26 | | df-br 4005 |
. . . . . . . . . . 11
                        |
27 | 25, 26 | sylnib 676 |
. . . . . . . . . 10
   EXMID TAp


        
             |
28 | 17, 27 | eqneltrrd 2274 |
. . . . . . . . 9
   EXMID TAp


        
             |
29 | 15, 28 | pm2.65da 661 |
. . . . . . . 8
  EXMID TAp


          |
30 | 29 | neqned 2354 |
. . . . . . 7
  EXMID TAp


          |
31 | 11, 13, 30 | jca31 309 |
. . . . . 6
  EXMID TAp


                      |
32 | | eleq1 2240 |
. . . . . . . . . 10
    

       |
33 | | eleq1 2240 |
. . . . . . . . . 10
    

       |
34 | 32, 33 | bi2anan9 606 |
. . . . . . . . 9
            
              |
35 | | simpl 109 |
. . . . . . . . . 10
                 |
36 | | simpr 110 |
. . . . . . . . . 10
                 |
37 | 35, 36 | neeq12d 2367 |
. . . . . . . . 9
           
           |
38 | 34, 37 | anbi12d 473 |
. . . . . . . 8
               
                       |
39 | 38 | opelopabga 4264 |
. . . . . . 7
                               
                       |
40 | 11, 13, 39 | syl2anc 411 |
. . . . . 6
  EXMID TAp


                 

 
                       |
41 | 31, 40 | mpbird 167 |
. . . . 5
  EXMID TAp


                

    |
42 | 9, 41 | eqeltrd 2254 |
. . . 4
  EXMID TAp


           |
43 | | relopab 4754 |
. . . . . . 7
          |
44 | | 1st2nd 6182 |
. . . . . . 7
       

 
     

                |
45 | 43, 44 | mpan 424 |
. . . . . 6
      

               |
46 | 45 | adantl 277 |
. . . . 5
  EXMID TAp

     

                |
47 | | breq2 4008 |
. . . . . . . . . 10
    
                    |
48 | 47 | notbid 667 |
. . . . . . . . 9
    
      
             |
49 | | eqeq2 2187 |
. . . . . . . . 9
    
                |
50 | 48, 49 | imbi12d 234 |
. . . . . . . 8
    
                                    |
51 | | breq1 4007 |
. . . . . . . . . . . 12
    
  
         |
52 | 51 | notbid 667 |
. . . . . . . . . . 11
    
  
         |
53 | | eqeq1 2184 |
. . . . . . . . . . 11
    

       |
54 | 52, 53 | imbi12d 234 |
. . . . . . . . . 10
    
   
                |
55 | 54 | ralbidv 2477 |
. . . . . . . . 9
    
 
  
                 |
56 | 4 | simp3d 1011 |
. . . . . . . . . . 11
 TAp
 


          

  
    |
57 | 56 | simprd 114 |
. . . . . . . . . 10
 TAp


      |
58 | 57 | ad2antlr 489 |
. . . . . . . . 9
  EXMID TAp

     

    

 
   |
59 | 32 | anbi1d 465 |
. . . . . . . . . . . . . 14
    
 
     
    |
60 | | neeq1 2360 |
. . . . . . . . . . . . . 14
    

       |
61 | 59, 60 | anbi12d 473 |
. . . . . . . . . . . . 13
    
  


     
         |
62 | 33 | anbi2d 464 |
. . . . . . . . . . . . . 14
    
     
              |
63 | | neeq2 2361 |
. . . . . . . . . . . . . 14
    
                |
64 | 62, 63 | anbi12d 473 |
. . . . . . . . . . . . 13
    
      
                             |
65 | 61, 64 | elopabi 6196 |
. . . . . . . . . . . 12
      

                        |
66 | 65 | adantl 277 |
. . . . . . . . . . 11
  EXMID TAp

     

                         |
67 | 66 | simpld 112 |
. . . . . . . . . 10
  EXMID TAp

     

               |
68 | 67 | simpld 112 |
. . . . . . . . 9
  EXMID TAp

     

         |
69 | 55, 58, 68 | rspcdva 2847 |
. . . . . . . 8
  EXMID TAp

     

    
             |
70 | 67 | simprd 114 |
. . . . . . . 8
  EXMID TAp

     

         |
71 | 50, 69, 70 | rspcdva 2847 |
. . . . . . 7
  EXMID TAp

     

             
           |
72 | 66 | simprd 114 |
. . . . . . . 8
  EXMID TAp

     

             |
73 | 72 | neneqd 2368 |
. . . . . . 7
  EXMID TAp

     

  
          |
74 | | exmidexmid 4197 |
. . . . . . . . 9
EXMID
DECID             |
75 | | con1dc 856 |
. . . . . . . . 9
DECID                                                       |
76 | 74, 75 | syl 14 |
. . . . . . . 8
EXMID                                             |
77 | 76 | ad2antrr 488 |
. . . . . . 7
  EXMID TAp

     

                                               |
78 | 71, 73, 77 | mp2d 47 |
. . . . . 6
  EXMID TAp

     

               |
79 | | df-br 4005 |
. . . . . 6
                        |
80 | 78, 79 | sylib 122 |
. . . . 5
  EXMID TAp

     

                |
81 | 46, 80 | eqeltrd 2254 |
. . . 4
  EXMID TAp

     

     |
82 | 42, 81 | impbida 596 |
. . 3
 EXMID TAp        

     |
83 | 82 | eqrdv 2175 |
. 2
 EXMID TAp 
     

    |
84 | | exmidexmid 4197 |
. . . . . . 7
EXMID
DECID
  |
85 | 84 | ralrimivw 2551 |
. . . . . 6
EXMID 
DECID
  |
86 | 85 | ralrimivw 2551 |
. . . . 5
EXMID 

DECID
  |
87 | | netap 7253 |
. . . . 5
 

DECID
     

  TAp   |
88 | 86, 87 | syl 14 |
. . . 4
EXMID      

  TAp   |
89 | 88 | adantr 276 |
. . 3
 EXMID      

        

  TAp   |
90 | | tapeq1 7251 |
. . . 4
      

   TAp
     

  TAp    |
91 | 90 | adantl 277 |
. . 3
 EXMID      

    TAp          TAp    |
92 | 89, 91 | mpbird 167 |
. 2
 EXMID      

   TAp
  |
93 | 83, 92 | impbida 596 |
1
EXMID  TAp
            |