Theorem necomi

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

	Ref	Expression
Hypothesis	necomi.1	⊢ 𝐴 ≠ 𝐵
Assertion	necomi	⊢ 𝐵 ≠ 𝐴

Proof

Step	Hyp	Ref	Expression
1		necomi.1	⊢ 𝐴 ≠ 𝐵
2		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
3	1 2	mpbi	⊢ 𝐵 ≠ 𝐴