Theorem nesym 3002

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2945

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 1975  ax-7 2015  ax-9 2120  ax-ext 2711

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

This theorem is referenced by:  0nelopabOLD  5482  fiming  9235  wemapsolem  9287  nn01to3  12680  xrltlen  12879  sgnn  14803  isprm3  16386  lspsncv0  20406  uvcvv0  20995  fvmptnn04if  21996  chfacfisf  22001  chfacfisfcpmat  22002  trfbas  22993  fbunfip  23018  trfil2  23036  iundisj2  24711  pthdlem2lem  28131  fusgr2wsp2nb  28694  iundisj2f  30925  iundisj2fi  31114  cvmscld  33231  nosupbnd2lem1  33914  noinfbnd2lem1  33929  poimirlem25  35798  hlrelat5N  37411  cmpfiiin  40516  gneispace  41714  iblcncfioo  43490  fourierdlem82  43700  elprneb  44491  fzopredsuc  44784  iccpartiltu  44843