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  8424  ord2eln012  8425  fiming  9406  wemapsolem  9458  nn01to3  12882  xrltlen  13088  sgnn  15047  isprm3  16643  lspsncv0  21136  uvcvv0  21780  fvmptnn04if  22824  chfacfisf  22829  chfacfisfcpmat  22830  trfbas  23819  fbunfip  23844  trfil2  23862  iundisj2  25526  nosupbnd2lem1  27693  noinfbnd2lem1  27708  elnns2  28347  pthdlem2lem  29850  fusgr2wsp2nb  30419  iundisj2f  32675  iundisj2fi  32885  cvmscld  35471  poimirlem25  37980  hlrelat5N  39861  redvmptabs  42806  cmpfiiin  43143  gneispace  44579  iblcncfioo  46424  fourierdlem82  46634  elprneb  47489  fzopredsuc  47784  iccpartiltu  47894