Metamath Proof Explorer


Theorem necomi

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

Ref Expression
Hypothesis necomi.1 A B
Assertion necomi B A

Proof

Step Hyp Ref Expression
1 necomi.1 A B
2 necom A B B A
3 1 2 mpbi B A