Theorem nesym 2982

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

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

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 2702

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

This theorem is referenced by:  ord1eln01  8463  ord2eln012  8464  fiming  9458  wemapsolem  9510  nn01to3  12907  xrltlen  13113  sgnn  15067  isprm3  16660  lspsncv0  21063  uvcvv0  21706  fvmptnn04if  22743  chfacfisf  22748  chfacfisfcpmat  22749  trfbas  23738  fbunfip  23763  trfil2  23781  iundisj2  25457  nosupbnd2lem1  27634  noinfbnd2lem1  27649  elnns2  28240  pthdlem2lem  29704  fusgr2wsp2nb  30270  iundisj2f  32526  iundisj2fi  32727  cvmscld  35267  poimirlem25  37646  hlrelat5N  39402  redvmptabs  42355  cmpfiiin  42692  gneispace  44130  iblcncfioo  45983  fourierdlem82  46193  elprneb  47034  fzopredsuc  47328  iccpartiltu  47427