Metamath Proof Explorer


Theorem necomi

Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012)

Ref Expression
Hypothesis necomi.1 AB
Assertion necomi BA

Proof

Step Hyp Ref Expression
1 necomi.1 AB
2 necom ABBA
3 1 2 mpbi BA