Theorem nesym 3000

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  0nelopabOLD  5481  ord1eln01  8326  ord2eln012  8327  fiming  9257  wemapsolem  9309  nn01to3  12681  xrltlen  12880  sgnn  14805  isprm3  16388  lspsncv0  20408  uvcvv0  20997  fvmptnn04if  21998  chfacfisf  22003  chfacfisfcpmat  22004  trfbas  22995  fbunfip  23020  trfil2  23038  iundisj2  24713  pthdlem2lem  28135  fusgr2wsp2nb  28698  iundisj2f  30929  iundisj2fi  31118  cvmscld  33235  nosupbnd2lem1  33918  noinfbnd2lem1  33933  poimirlem25  35802  hlrelat5N  37415  cmpfiiin  40519  gneispace  41744  iblcncfioo  43519  fourierdlem82  43729  elprneb  44523  fzopredsuc  44815  iccpartiltu  44874