Theorem nesym 3072

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  0nelopab  5444  fiming  8956  wemapsolem  9008  nn01to3  12335  xrltlen  12533  sgnn  14447  pwm1geoserOLD  15219  isprm3  16021  lspsncv0  19912  uvcvv0  20928  fvmptnn04if  21451  chfacfisf  21456  chfacfisfcpmat  21457  trfbas  22446  fbunfip  22471  trfil2  22489  iundisj2  24144  pthdlem2lem  27542  fusgr2wsp2nb  28107  iundisj2f  30334  iundisj2fi  30514  cvmscld  32515  nosupbnd2lem1  33210  poimirlem25  34911  hlrelat5N  36531  cmpfiiin  39287  gneispace  40477  iblcncfioo  42256  fourierdlem82  42467  elprneb  43258  fzopredsuc  43517  iccpartiltu  43576