Theorem nesym 3016

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  iunopeqop  5495  ord1eln01  8469  ord2eln012  8470  fiming  9448  wemapsolem  9500  nn01to3  12956  xrltlen  13162  sgnn  15121  isprm3  16731  lspsncv0  21239  uvcvv0  21900  fvmptnn04if  22967  chfacfisf  22972  chfacfisfcpmat  22973  trfbas  23962  fbunfip  23987  trfil2  24005  iundisj2  25669  nosupbnd2lem1  27837  noinfbnd2lem1  27852  elnns2  28492  pthdlem2lem  30025  fusgr2wsp2nb  30594  iundisj2f  32845  iundisj2fi  33054  cvmscld  35636  poimirlem25  38156  hlrelat5N  40037  redvmptabs  42981  cmpfiiin  43290  gneispace  44722  iblcncfioo  46550  fourierdlem82  46760  elprneb  47621  fzopredsuc  47916  iccpartiltu  48026