Theorem nesym 2985

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  ord1eln01  8417  ord2eln012  8418  fiming  9391  wemapsolem  9443  nn01to3  12841  xrltlen  13047  sgnn  15003  isprm3  16596  lspsncv0  21085  uvcvv0  21729  fvmptnn04if  22765  chfacfisf  22770  chfacfisfcpmat  22771  trfbas  23760  fbunfip  23785  trfil2  23803  iundisj2  25478  nosupbnd2lem1  27655  noinfbnd2lem1  27670  elnns2  28270  pthdlem2lem  29747  fusgr2wsp2nb  30316  iundisj2f  32572  iundisj2fi  32784  cvmscld  35338  poimirlem25  37705  hlrelat5N  39520  redvmptabs  42478  cmpfiiin  42814  gneispace  44251  iblcncfioo  46100  fourierdlem82  46310  elprneb  47153  fzopredsuc  47447  iccpartiltu  47546