Theorem nesym 2988

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  ord1eln01  8423  ord2eln012  8424  fiming  9403  wemapsolem  9455  nn01to3  12854  xrltlen  13060  sgnn  15017  isprm3  16610  lspsncv0  21101  uvcvv0  21745  fvmptnn04if  22793  chfacfisf  22798  chfacfisfcpmat  22799  trfbas  23788  fbunfip  23813  trfil2  23831  iundisj2  25506  nosupbnd2lem1  27683  noinfbnd2lem1  27698  elnns2  28337  pthdlem2lem  29840  fusgr2wsp2nb  30409  iundisj2f  32665  iundisj2fi  32877  cvmscld  35467  poimirlem25  37842  hlrelat5N  39657  redvmptabs  42611  cmpfiiin  42935  gneispace  44371  iblcncfioo  46218  fourierdlem82  46428  elprneb  47271  fzopredsuc  47565  iccpartiltu  47664