Theorem nesym 3039

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1522   ≠ wne 2983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1763  df-cleq 2787  df-ne 2984

This theorem is referenced by:  0nelopab  5343  fiming  8811  wemapsolem  8863  nn01to3  12190  xrltlen  12389  sgnn  14287  pwm1geoserOLD  15058  isprm3  15856  lspsncv0  19608  uvcvv0  20616  fvmptnn04if  21141  chfacfisf  21146  chfacfisfcpmat  21147  trfbas  22136  fbunfip  22161  trfil2  22179  iundisj2  23833  pthdlem2lem  27230  fusgr2wsp2nb  27797  iundisj2f  30022  iundisj2fi  30198  cvmscld  32122  nosupbnd2lem1  32818  poimirlem25  34461  hlrelat5N  36081  cmpfiiin  38792  gneispace  39982  iblcncfioo  41818  fourierdlem82  42029  elprneb  42794  fzopredsuc  43053  iccpartiltu  43078