Description: Contrapositive inference for inequality. (Contributed by NM, 31Jan2008)
Ref  Expression  

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

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

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

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

3  2 1  bitr3id   ( ph > ( . A = B <> ps ) ) 
4  3  con1bid   ( ph > ( . ps <> A = B ) ) 