Theorem nesym 3012

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  iunopeqop  5489  ord1eln01  8460  ord2eln012  8461  fiming  9443  wemapsolem  9495  nn01to3  12939  xrltlen  13145  sgnn  15104  isprm3  16700  lspsncv0  21196  uvcvv0  21822  fvmptnn04if  22889  chfacfisf  22894  chfacfisfcpmat  22895  trfbas  23884  fbunfip  23909  trfil2  23927  iundisj2  25591  nosupbnd2lem1  27756  noinfbnd2lem1  27771  elnns2  28411  pthdlem2lem  29913  fusgr2wsp2nb  30482  iundisj2f  32739  iundisj2fi  32949  cvmscld  35587  poimirlem25  38108  hlrelat5N  39989  redvmptabs  42933  cmpfiiin  43242  gneispace  44674  iblcncfioo  46516  fourierdlem82  46726  elprneb  47587  fzopredsuc  47882  iccpartiltu  47992