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	$$⊢\neg A=B$$
Assertion	nesymir	$$⊢B\ne A$$

Proof

Step	Hyp	Ref	Expression
1		nesymir.1	$$⊢\neg A=B$$
2	1	neir	$$⊢A\ne B$$
3	2	necomi	$$⊢B\ne A$$