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

Hypothesis  necon3bd.1   ( ph > ( A = B > ps ) ) 

Assertion  necon3bd   ( ph > ( . ps > A =/= B ) ) 
Step  Hyp  Ref  Expression 

1  necon3bd.1   ( ph > ( A = B > ps ) ) 

2  nne   ( . A =/= B <> A = B ) 

3  2 1  syl5bi   ( ph > ( . A =/= B > ps ) ) 
4  3  con1d   ( ph > ( . ps > A =/= B ) ) 