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

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

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

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

2  neneq   ( A =/= B > . A = B ) 

3  1 2  nsyli   ( ph > ( A =/= B > . ps ) ) 