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

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

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

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

2  notnot   ( ps > . . ps ) 

3  1  necon3bd   ( ph > ( . . ps > A =/= B ) ) 
4  2 3  syl5   ( ph > ( ps > A =/= B ) ) 