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 1542   ≠ 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  4369  raldifsnb  4754  tpprceq3  4762  tppreqb  4763  prneimg  4812  prnebg  4814  xpeq0  6126  xpcan  6142  xpcan2  6143  fndmdifeq0  6998  ftpg  7111  fnnfpeq0  7134  suppimacnv  8126  fnsuppres  8143  suppcoss  8159  ixp0  8881  isfin5-2  10313  zornn0g  10427  nn0n0n1ge2b  12482  fsuppmapnn0fiub0  13928  fsuppmapnn0ub  13930  mptnn0fsupp  13932  mptnn0fsuppr  13934  discr  14175  hashgt12el  14357  hashgt12el2  14358  hashtpg  14420  hash3tpde  14428  fprodle  15931  alzdvds  16259  algcvgblem  16516  lcmfunsnlem2lem2  16578  mndpsuppss  18702  lssne0  20914  dsmm0cl  21707  pmatcollpw2lem  22733  elcls  23029  cmpfi  23364  bwth  23366  1stccnp  23418  dissnlocfin  23485  trfil3  23844  isufil2  23864  bcth3  25299  rrxmvallem  25372  mdegleb  26037  tglowdim1i  28585  tglineintmo  28726  lmieu  28868  uhgrvd00  29620  wlkon2n0  29750  wwlks  29920  rusgrnumwwlks  30062  clwwlkneq0  30116  1to2vfriswmgr  30366  numclwwlk3lem2  30471  frgrregord013  30482  nmlno0lem  30881  lnon0  30886  nmlnop0iALT  32083  atom1d  32441  n0nsnel  32602  uniinn0  32637  nfpconfp  32722  funcnv5mpt  32757  suppiniseg  32776  xaddeq0  32844  pmtrcnel  33183  1arithidom  33630  esplymhp  33745  fedgmullem2  33808  irredminply  33894  zarcls1  34047  bnj1533  35028  bnj1541  35032  bnj1279  35194  bnj1280  35196  bnj1311  35200  spthcycl  35345  nepss  35934  bj-ismooredr2  37363  nlpineqsn  37663  poimirlem31  37902  poimirlem32  37903  itg2addnclem2  37923  ftc1anc  37952  n0elqs  38583  suceldisj  39069  lfl1  39446  lkreqN  39546  pmap0  40141  paddasslem17  40212  ltrnnid  40512  sticksstones1  42516  dffltz  42992  dflim5  43686  ntrneikb  44450  fzdifsuc2  45672  limclr  46013  liminflbuz2  46173  fourierdlem42  46507  fourierdlem76  46540  sge0cl  46739  meadjiunlem  46823  smfpimne2  47198  chnerlem1  47240  n0nsn2el  47385  oddprmne2  48075  usgrexmpl2trifr  48397  islininds2  48844  line2ylem  49111  line2xlem  49113  itsclc0xyqsol  49128  2itscp  49141  dmrnxp  49196  fdomne0  49209  oppcendc  49377