Description: Contrapositive inference for inequality. (Contributed by NM, 9Aug2006) (Proof shortened by Wolf Lammen, 22Nov2019)
Ref  Expression  

Hypothesis  necon3i.1   ( A = B > C = D ) 

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

1  necon3i.1   ( A = B > C = D ) 

2  1  necon3ai   ( C =/= D > . A = B ) 
3  2  neqned   ( C =/= D > A =/= B ) 