Description: Contrapositive deduction for inequality. (Contributed by NM, 13Apr2007) (Proof shortened by Wolf Lammen, 24Nov2019)
Ref  Expression  

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

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

1  necon2bbid.1   ( ph > ( ps <> A =/= B ) ) 

2  notnotb   ( ps <> . . ps ) 

3  1 2  bitr3di   ( ph > ( A =/= B <> . . ps ) ) 
4  3  necon4abid   ( ph > ( A = B <> . ps ) ) 