Theorem nesym 2989

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 2979	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  ord1eln01  8513  ord2eln012  8514  fiming  9517  wemapsolem  9569  nn01to3  12962  xrltlen  13167  sgnn  15118  isprm3  16707  lspsncv0  21112  uvcvv0  21755  fvmptnn04if  22792  chfacfisf  22797  chfacfisfcpmat  22798  trfbas  23787  fbunfip  23812  trfil2  23830  iundisj2  25507  nosupbnd2lem1  27684  noinfbnd2lem1  27699  elnns2  28290  pthdlem2lem  29754  fusgr2wsp2nb  30320  iundisj2f  32576  iundisj2fi  32779  cvmscld  35300  poimirlem25  37674  hlrelat5N  39425  redvmptabs  42370  cmpfiiin  42687  gneispace  44125  iblcncfioo  45974  fourierdlem82  46184  elprneb  47025  fzopredsuc  47319  iccpartiltu  47403