Theorem nesymi

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

	Ref	Expression
Hypothesis	nesymi.1	$$⊢A\ne B$$
Assertion	nesymi	$$⊢\neg B=A$$

Proof

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