Theorem nesym 2981

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

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

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 2701

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

This theorem is referenced by:  ord1eln01  8421  ord2eln012  8422  fiming  9409  wemapsolem  9461  nn01to3  12860  xrltlen  13066  sgnn  15019  isprm3  16612  lspsncv0  21071  uvcvv0  21715  fvmptnn04if  22752  chfacfisf  22757  chfacfisfcpmat  22758  trfbas  23747  fbunfip  23772  trfil2  23790  iundisj2  25466  nosupbnd2lem1  27643  noinfbnd2lem1  27658  elnns2  28256  pthdlem2lem  29730  fusgr2wsp2nb  30296  iundisj2f  32552  iundisj2fi  32753  cvmscld  35245  poimirlem25  37624  hlrelat5N  39380  redvmptabs  42333  cmpfiiin  42670  gneispace  44107  iblcncfioo  45960  fourierdlem82  46170  elprneb  47014  fzopredsuc  47308  iccpartiltu  47407