Theorem nne 2937

Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)

Assertion

Ref	Expression
nne	⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 357	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 224	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ne 2934

This theorem is referenced by:  neirr  2942  necon3bd  2947  necon1d  2955  necon4d  2957  necon4bid  2978  necon1bbii  2982  pm2.61ine  3016  ne3anior  3027  sbcne12  4395  raldifsnb  4777  tpprceq3  4785  tppreqb  4786  prneimg  4835  prnebg  4837  xpeq0  6154  xpcan  6170  xpcan2  6171  fndmdifeq0  7039  ftpg  7151  fnnfpeq0  7175  suppimacnv  8178  fnsuppres  8195  suppcoss  8211  ixp0  8950  isfin5-2  10410  zornn0g  10524  nn0n0n1ge2b  12575  fsuppmapnn0fiub0  14016  fsuppmapnn0ub  14018  mptnn0fsupp  14020  mptnn0fsuppr  14022  discr  14263  hashgt12el  14445  hashgt12el2  14446  hashtpg  14508  hash3tpde  14516  fprodle  16017  alzdvds  16344  algcvgblem  16601  lcmfunsnlem2lem2  16663  mndpsuppss  18748  lssne0  20913  dsmm0cl  21705  pmatcollpw2lem  22720  elcls  23016  cmpfi  23351  bwth  23353  1stccnp  23405  dissnlocfin  23472  trfil3  23831  isufil2  23851  bcth3  25288  rrxmvallem  25361  mdegleb  26026  tglowdim1i  28485  tglineintmo  28626  lmieu  28768  uhgrvd00  29519  wlkon2n0  29651  wwlks  29822  rusgrnumwwlks  29961  clwwlkneq0  30015  1to2vfriswmgr  30265  numclwwlk3lem2  30370  frgrregord013  30381  nmlno0lem  30779  lnon0  30784  nmlnop0iALT  31981  atom1d  32339  n0nsnel  32501  uniinn0  32536  nfpconfp  32615  funcnv5mpt  32651  suppiniseg  32668  xaddeq0  32735  pmtrcnel  33105  1arithidom  33557  fedgmullem2  33675  irredminply  33755  zarcls1  33905  bnj1533  34888  bnj1541  34892  bnj1279  35054  bnj1280  35056  bnj1311  35060  spthcycl  35156  nepss  35740  bj-ismooredr2  37133  nlpineqsn  37431  poimirlem31  37680  poimirlem32  37681  itg2addnclem2  37701  ftc1anc  37730  n0elqs  38349  lfl1  39093  lkreqN  39193  pmap0  39789  paddasslem17  39860  ltrnnid  40160  sticksstones1  42164  dffltz  42632  dflim5  43328  ntrneikb  44093  fzdifsuc2  45319  limclr  45664  liminflbuz2  45824  fourierdlem42  46158  fourierdlem76  46191  sge0cl  46390  meadjiunlem  46474  smfpimne2  46849  n0nsn2el  47034  oddprmne2  47709  usgrexmpl2trifr  48021  islininds2  48440  line2ylem  48711  line2xlem  48713  itsclc0xyqsol  48728  2itscp  48741  dmrnxp  48795  fdomne0  48808  oppcendc  48973