Theorem nesym 2988

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  iunopeqop  5475  ord1eln01  8431  ord2eln012  8432  fiming  9413  wemapsolem  9465  nn01to3  12891  xrltlen  13097  sgnn  15056  isprm3  16652  lspsncv0  21144  uvcvv0  21770  fvmptnn04if  22814  chfacfisf  22819  chfacfisfcpmat  22820  trfbas  23809  fbunfip  23834  trfil2  23852  iundisj2  25516  nosupbnd2lem1  27679  noinfbnd2lem1  27694  elnns2  28333  pthdlem2lem  29835  fusgr2wsp2nb  30404  iundisj2f  32660  iundisj2fi  32870  cvmscld  35455  poimirlem25  37966  hlrelat5N  39847  redvmptabs  42792  cmpfiiin  43129  gneispace  44561  iblcncfioo  46406  fourierdlem82  46616  elprneb  47477  fzopredsuc  47772  iccpartiltu  47882