Theorem nesym 2999

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  0nelopabOLD  5472  fiming  9187  wemapsolem  9239  nn01to3  12610  xrltlen  12809  sgnn  14733  isprm3  16316  lspsncv0  20323  uvcvv0  20907  fvmptnn04if  21906  chfacfisf  21911  chfacfisfcpmat  21912  trfbas  22903  fbunfip  22928  trfil2  22946  iundisj2  24618  pthdlem2lem  28036  fusgr2wsp2nb  28599  iundisj2f  30830  iundisj2fi  31020  cvmscld  33135  nosupbnd2lem1  33845  noinfbnd2lem1  33860  poimirlem25  35729  hlrelat5N  37342  cmpfiiin  40435  gneispace  41633  iblcncfioo  43409  fourierdlem82  43619  elprneb  44410  fzopredsuc  44703  iccpartiltu  44762