Theorem nesym 2981

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

Assertion

Ref	Expression
nesym	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

Proof of Theorem nesym

Step	Hyp	Ref	Expression
1		eqcom 2736	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3abii 2971	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  ord1eln01  8460  ord2eln012  8461  fiming  9451  wemapsolem  9503  nn01to3  12900  xrltlen  13106  sgnn  15060  isprm3  16653  lspsncv0  21056  uvcvv0  21699  fvmptnn04if  22736  chfacfisf  22741  chfacfisfcpmat  22742  trfbas  23731  fbunfip  23756  trfil2  23774  iundisj2  25450  nosupbnd2lem1  27627  noinfbnd2lem1  27642  elnns2  28233  pthdlem2lem  29697  fusgr2wsp2nb  30263  iundisj2f  32519  iundisj2fi  32720  cvmscld  35260  poimirlem25  37639  hlrelat5N  39395  redvmptabs  42348  cmpfiiin  42685  gneispace  44123  iblcncfioo  45976  fourierdlem82  46186  elprneb  47030  fzopredsuc  47324  iccpartiltu  47423