Metamath Proof Explorer


Theorem necomd

Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008)

Ref Expression
Hypothesis necomd.1 φ A B
Assertion necomd φ B A

Proof

Step Hyp Ref Expression
1 necomd.1 φ A B
2 necom A B B A
3 1 2 sylib φ B A