Theorem nesym 2994

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1534   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ne 2938

This theorem is referenced by:  0nelopabOLD  5570  ord1eln01  8517  ord2eln012  8518  fiming  9522  wemapsolem  9574  nn01to3  12956  xrltlen  13158  sgnn  15074  isprm3  16654  lspsncv0  21034  uvcvv0  21724  fvmptnn04if  22764  chfacfisf  22769  chfacfisfcpmat  22770  trfbas  23761  fbunfip  23786  trfil2  23804  iundisj2  25491  nosupbnd2lem1  27661  noinfbnd2lem1  27676  elnns2  28222  pthdlem2lem  29594  fusgr2wsp2nb  30157  iundisj2f  32393  iundisj2fi  32578  cvmscld  34883  poimirlem25  37118  hlrelat5N  38874  cmpfiiin  42117  gneispace  43564  iblcncfioo  45366  fourierdlem82  45576  elprneb  46411  fzopredsuc  46703  iccpartiltu  46762