Theorem nesym 2996

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1539   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940

This theorem is referenced by:  ord1eln01  8535  ord2eln012  8536  fiming  9539  wemapsolem  9591  nn01to3  12984  xrltlen  13189  sgnn  15134  isprm3  16721  lspsncv0  21149  uvcvv0  21811  fvmptnn04if  22856  chfacfisf  22861  chfacfisfcpmat  22862  trfbas  23853  fbunfip  23878  trfil2  23896  iundisj2  25585  nosupbnd2lem1  27761  noinfbnd2lem1  27776  elnns2  28345  pthdlem2lem  29788  fusgr2wsp2nb  30354  iundisj2f  32604  iundisj2fi  32800  cvmscld  35279  poimirlem25  37653  hlrelat5N  39404  redvmptabs  42395  cmpfiiin  42713  gneispace  44152  iblcncfioo  45998  fourierdlem82  46208  elprneb  47046  fzopredsuc  47340  iccpartiltu  47414