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

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

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

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

2  1  necon2bd   ( ph > ( C = D > . A =/= B ) ) 
3  nne   ( . A =/= B <> A = B ) 

4  2 3  syl6ib   ( ph > ( C = D > A = B ) ) 