Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30Nov2011)
Ref  Expression  

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

pm2.61dane.2   ( ( ph /\ A =/= B ) > ps ) 

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

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

2  pm2.61dane.2   ( ( ph /\ A =/= B ) > ps ) 

3  1  ex   ( ph > ( A = B > ps ) ) 
4  2  ex   ( ph > ( A =/= B > ps ) ) 
5  3 4  pm2.61dne   ( ph > ps ) 