Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29May2013)
Ref  Expression  

Hypotheses  pm2.61da2ne.1   ( ( ph /\ A = B ) > ps ) 

pm2.61da2ne.2   ( ( ph /\ C = D ) > ps ) 

pm2.61da2ne.3   ( ( ph /\ ( A =/= B /\ C =/= D ) ) > ps ) 

Assertion  pm2.61da2ne   ( ph > ps ) 
Step  Hyp  Ref  Expression 

1  pm2.61da2ne.1   ( ( ph /\ A = B ) > ps ) 

2  pm2.61da2ne.2   ( ( ph /\ C = D ) > ps ) 

3  pm2.61da2ne.3   ( ( ph /\ ( A =/= B /\ C =/= D ) ) > ps ) 

4  2  adantlr   ( ( ( ph /\ A =/= B ) /\ C = D ) > ps ) 
5  3  anassrs   ( ( ( ph /\ A =/= B ) /\ C =/= D ) > ps ) 
6  4 5  pm2.61dane   ( ( ph /\ A =/= B ) > ps ) 
7  1 6  pm2.61dane   ( ph > ps ) 