Theorem nesym 2991

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  iunopeqop  5469  ord1eln01  8428  ord2eln012  8429  fiming  9410  wemapsolem  9462  nn01to3  12889  xrltlen  13095  sgnn  15054  isprm3  16650  lspsncv0  21146  uvcvv0  21772  fvmptnn04if  22839  chfacfisf  22844  chfacfisfcpmat  22845  trfbas  23834  fbunfip  23859  trfil2  23877  iundisj2  25541  nosupbnd2lem1  27704  noinfbnd2lem1  27719  elnns2  28358  pthdlem2lem  29860  fusgr2wsp2nb  30429  iundisj2f  32686  iundisj2fi  32896  cvmscld  35508  poimirlem25  38019  hlrelat5N  39900  redvmptabs  42844  cmpfiiin  43153  gneispace  44585  iblcncfioo  46428  fourierdlem82  46638  elprneb  47499  fzopredsuc  47794  iccpartiltu  47904