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