Description: Contrapositive deduction for inequality. (Contributed by NM, 21Mar2007) (Proof shortened by Andrew Salmon, 25May2011) (Proof shortened by Wolf Lammen, 23Nov2019)
Ref  Expression  

Hypothesis  necon1bd.1   ( ph > ( A =/= B > ps ) ) 

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

1  necon1bd.1   ( ph > ( A =/= B > ps ) ) 

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

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