Description: Contrapositive law deduction for inequality. (Contributed by NM, 28Dec2008) (Proof shortened by Andrew Salmon, 25May2011)
Ref  Expression  

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

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

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

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

3  1 2  syl6ibr   ( ph > ( A =/= B > . C =/= D ) ) 
4  3  necon4ad   ( ph > ( C =/= D > A = B ) ) 