Theorem nesym 2989

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 2744	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3abii 2979	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  ord1eln01  8433  ord2eln012  8434  fiming  9415  wemapsolem  9467  nn01to3  12866  xrltlen  13072  sgnn  15029  isprm3  16622  lspsncv0  21113  uvcvv0  21757  fvmptnn04if  22805  chfacfisf  22810  chfacfisfcpmat  22811  trfbas  23800  fbunfip  23825  trfil2  23843  iundisj2  25518  nosupbnd2lem1  27695  noinfbnd2lem1  27710  elnns2  28349  pthdlem2lem  29852  fusgr2wsp2nb  30421  iundisj2f  32676  iundisj2fi  32887  cvmscld  35486  poimirlem25  37890  hlrelat5N  39771  redvmptabs  42724  cmpfiiin  43048  gneispace  44484  iblcncfioo  46330  fourierdlem82  46540  elprneb  47383  fzopredsuc  47677  iccpartiltu  47776