Description: Contrapositive inference for inequality. (Contributed by NM, 17Mar2007) (Proof shortened by Wolf Lammen, 24Nov2019)
Ref  Expression  

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

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

1  necon1bbii.1   ( A =/= B <> ph ) 

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

3  2 1  xchnxbi   ( . ph <> A = B ) 