Description: Contrapositive inference for inequality. (Contributed by NM, 28Dec2008)
Ref  Expression  

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

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

1  necon2d.1   ( ph > ( A = B > C =/= D ) ) 

2  dfne   ( C =/= D <> . C = D ) 

3  1 2  syl6ib   ( ph > ( A = B > . C = D ) ) 
4  3  necon2ad   ( ph > ( C = D > A =/= B ) ) 