Theorem nesym 2998

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  0nelopabOLD  5569  ord1eln01  8496  ord2eln012  8497  fiming  9493  wemapsolem  9545  nn01to3  12925  xrltlen  13125  sgnn  15041  isprm3  16620  lspsncv0  20759  uvcvv0  21345  fvmptnn04if  22351  chfacfisf  22356  chfacfisfcpmat  22357  trfbas  23348  fbunfip  23373  trfil2  23391  iundisj2  25066  nosupbnd2lem1  27218  noinfbnd2lem1  27233  pthdlem2lem  29024  fusgr2wsp2nb  29587  iundisj2f  31821  iundisj2fi  32008  cvmscld  34264  poimirlem25  36513  hlrelat5N  38272  cmpfiiin  41435  gneispace  42885  iblcncfioo  44694  fourierdlem82  44904  elprneb  45739  fzopredsuc  46031  iccpartiltu  46090