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	⊢ 𝐴 ≠ 𝐵
Assertion	nesymi	⊢ ¬ 𝐵 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		nesymi.1	⊢ 𝐴 ≠ 𝐵
2	1	necomi	⊢ 𝐵 ≠ 𝐴
3	2	neii	⊢ ¬ 𝐵 = 𝐴