Theorem necomi

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

	Ref	Expression
Hypothesis	necomi.1	$$⊢A\ne B$$
Assertion	necomi	$$⊢B\ne A$$

Proof

Step	Hyp	Ref	Expression
1		necomi.1	$$⊢A\ne B$$
2		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
3	1 2	mpbi	$$⊢B\ne A$$