Description: Contrapositive law deduction for inequality. (Contributed by NM, 10Jun2006)
Ref  Expression  

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

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

1  necon3d.1   ( ph > ( A = B > C = D ) ) 

2  1  necon3ad   ( ph > ( C =/= D > . A = B ) ) 
3  dfne   ( A =/= B <> . A = B ) 

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