Theorem nesymir

Description: Inference associated with nesym . (Contributed by BJ, 7-Jul-2018) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Hypothesis	nesymir.1	⊢ ¬ 𝐴 = 𝐵
Assertion	nesymir	⊢ 𝐵 ≠ 𝐴

Proof

Step	Hyp	Ref	Expression
1		nesymir.1	⊢ ¬ 𝐴 = 𝐵
2	1	neir	⊢ 𝐴 ≠ 𝐵
3	2	necomi	⊢ 𝐵 ≠ 𝐴