Theorem nesym 2997

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541   ≠ wne 2940

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  0nelopabOLD  5567  ord1eln01  8492  ord2eln012  8493  fiming  9489  wemapsolem  9541  nn01to3  12921  xrltlen  13121  sgnn  15037  isprm3  16616  lspsncv0  20751  uvcvv0  21336  fvmptnn04if  22342  chfacfisf  22347  chfacfisfcpmat  22348  trfbas  23339  fbunfip  23364  trfil2  23382  iundisj2  25057  nosupbnd2lem1  27207  noinfbnd2lem1  27222  pthdlem2lem  29013  fusgr2wsp2nb  29576  iundisj2f  31808  iundisj2fi  31995  cvmscld  34252  poimirlem25  36501  hlrelat5N  38260  cmpfiiin  41420  gneispace  42870  iblcncfioo  44680  fourierdlem82  44890  elprneb  45725  fzopredsuc  46017  iccpartiltu  46076