Description: Contrapositive inference for inequality. (Contributed by NM, 18Mar2007)
Ref  Expression  

Hypothesis  necon1i.1   ( A =/= B > C = D ) 

Assertion  necon1i   ( C =/= D > A = B ) 
Step  Hyp  Ref  Expression 

1  necon1i.1   ( A =/= B > C = D ) 

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

3  2 1  sylbir   ( . A = B > C = D ) 
4  3  necon1ai   ( C =/= D > A = B ) 