This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nesym

Description: Characterization of inequality in terms of reversed equality (see bicom ). (Contributed by BJ, 7-Jul-2018)

Ref Expression
Assertion nesym ⊢ A ≠ B ↔ ¬ B = A

Proof

Step Hyp Ref Expression
1 eqcom ⊢ A = B ↔ B = A
2 1 necon3abii ⊢ A ≠ B ↔ ¬ B = A