Description: Inference from commutative law for inequality. (Contributed by NM, 17Oct2012)
Ref  Expression  

Hypothesis  necomi.1   A =/= B 

Assertion  necomi   B =/= A 
Step  Hyp  Ref  Expression 

1  necomi.1   A =/= B 

2  necom   ( A =/= B <> B =/= A ) 

3  1 2  mpbi   B =/= A 