Theorem nesym 3003

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  0nelopabOLD  5587  ord1eln01  8552  ord2eln012  8553  fiming  9567  wemapsolem  9619  nn01to3  13006  xrltlen  13208  sgnn  15143  isprm3  16730  lspsncv0  21171  uvcvv0  21833  fvmptnn04if  22876  chfacfisf  22881  chfacfisfcpmat  22882  trfbas  23873  fbunfip  23898  trfil2  23916  iundisj2  25603  nosupbnd2lem1  27778  noinfbnd2lem1  27793  elnns2  28362  pthdlem2lem  29803  fusgr2wsp2nb  30366  iundisj2f  32612  iundisj2fi  32802  cvmscld  35241  poimirlem25  37605  hlrelat5N  39358  cmpfiiin  42653  gneispace  44096  iblcncfioo  45899  fourierdlem82  46109  elprneb  46944  fzopredsuc  47238  iccpartiltu  47296