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  5568  ord1eln01  8498  ord2eln012  8499  fiming  9495  wemapsolem  9547  nn01to3  12929  xrltlen  13129  sgnn  15045  isprm3  16624  lspsncv0  20904  uvcvv0  21564  fvmptnn04if  22571  chfacfisf  22576  chfacfisfcpmat  22577  trfbas  23568  fbunfip  23593  trfil2  23611  iundisj2  25290  nosupbnd2lem1  27442  noinfbnd2lem1  27457  pthdlem2lem  29279  fusgr2wsp2nb  29842  iundisj2f  32076  iundisj2fi  32263  cvmscld  34550  poimirlem25  36816  hlrelat5N  38575  cmpfiiin  41737  gneispace  43187  iblcncfioo  44993  fourierdlem82  45203  elprneb  46038  fzopredsuc  46330  iccpartiltu  46389