Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16Jan2007) (Proof shortened by Andrew Salmon, 25May2011)
Ref  Expression  

Hypotheses  pm2.61ine.1   ( A = B > ph ) 

pm2.61ine.2   ( A =/= B > ph ) 

Assertion  pm2.61ine   ph 
Step  Hyp  Ref  Expression 

1  pm2.61ine.1   ( A = B > ph ) 

2  pm2.61ine.2   ( A =/= B > ph ) 

3  nne   ( . A =/= B <> A = B ) 

4  3 1  sylbi   ( . A =/= B > ph ) 
5  2 4  pm2.61i   ph 