Theorem nesym 2984

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  ord1eln01  8411  ord2eln012  8412  fiming  9384  wemapsolem  9436  nn01to3  12836  xrltlen  13042  sgnn  14998  isprm3  16591  lspsncv0  21081  uvcvv0  21725  fvmptnn04if  22762  chfacfisf  22767  chfacfisfcpmat  22768  trfbas  23757  fbunfip  23782  trfil2  23800  iundisj2  25475  nosupbnd2lem1  27652  noinfbnd2lem1  27667  elnns2  28267  pthdlem2lem  29743  fusgr2wsp2nb  30309  iundisj2f  32565  iundisj2fi  32774  cvmscld  35305  poimirlem25  37684  hlrelat5N  39439  redvmptabs  42392  cmpfiiin  42729  gneispace  44166  iblcncfioo  46015  fourierdlem82  46225  elprneb  47059  fzopredsuc  47353  iccpartiltu  47452