Description: Contrapositive inference for inequality. (Contributed by NM, 1Apr2007)
Ref  Expression  

Hypothesis  necon2bi.1   ( ph > A =/= B ) 

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

1  necon2bi.1   ( ph > A =/= B ) 

2  1  neneqd   ( ph > . A = B ) 
3  2  con2i   ( A = B > . ph ) 