Theorem nesym 2988

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1543   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  0nelopabOLD  5432  fiming  9092  wemapsolem  9144  nn01to3  12502  xrltlen  12701  sgnn  14622  isprm3  16203  lspsncv0  20137  uvcvv0  20706  fvmptnn04if  21700  chfacfisf  21705  chfacfisfcpmat  21706  trfbas  22695  fbunfip  22720  trfil2  22738  iundisj2  24400  pthdlem2lem  27808  fusgr2wsp2nb  28371  iundisj2f  30602  iundisj2fi  30792  cvmscld  32902  nosupbnd2lem1  33604  noinfbnd2lem1  33619  poimirlem25  35488  hlrelat5N  37101  cmpfiiin  40163  gneispace  41362  iblcncfioo  43137  fourierdlem82  43347  elprneb  44138  fzopredsuc  44431  iccpartiltu  44490