Description: Contrapositive inference for inequality. (Contributed by NM, 23May2007) (Proof shortened by Andrew Salmon, 25May2011)
Ref  Expression  

Hypothesis  necon3ai.1   ( ph > A = B ) 

Assertion  necon3ai   ( A =/= B > . ph ) 
Step  Hyp  Ref  Expression 

1  necon3ai.1   ( ph > A = B ) 

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

3  1 2  sylibr   ( ph > . A =/= B ) 
4  3  con2i   ( A =/= B > . ph ) 