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 1537   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

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

This theorem is referenced by:  0nelopab  5452  fiming  8962  wemapsolem  9014  nn01to3  12342  xrltlen  12540  sgnn  14453  pwm1geoserOLD  15225  isprm3  16027  lspsncv0  19918  uvcvv0  20934  fvmptnn04if  21457  chfacfisf  21462  chfacfisfcpmat  21463  trfbas  22452  fbunfip  22477  trfil2  22495  iundisj2  24150  pthdlem2lem  27548  fusgr2wsp2nb  28113  iundisj2f  30340  iundisj2fi  30520  cvmscld  32520  nosupbnd2lem1  33215  poimirlem25  34932  hlrelat5N  36552  cmpfiiin  39314  gneispace  40504  iblcncfioo  42283  fourierdlem82  42493  elprneb  43284  fzopredsuc  43543  iccpartiltu  43602