Theorem nne 2929

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 2926	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 357	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 224	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

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

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 2926

This theorem is referenced by:  neirr  2934  necon3bd  2939  necon1d  2947  necon4d  2949  necon4bid  2970  necon1bbii  2974  pm2.61ine  3008  ne3anior  3019  sbcne12  4374  raldifsnb  4756  tpprceq3  4764  tppreqb  4765  prneimg  4814  prnebg  4816  xpeq0  6121  xpcan  6137  xpcan2  6138  fndmdifeq0  6998  ftpg  7110  fnnfpeq0  7134  suppimacnv  8130  fnsuppres  8147  suppcoss  8163  ixp0  8881  isfin5-2  10320  zornn0g  10434  nn0n0n1ge2b  12487  fsuppmapnn0fiub0  13934  fsuppmapnn0ub  13936  mptnn0fsupp  13938  mptnn0fsuppr  13940  discr  14181  hashgt12el  14363  hashgt12el2  14364  hashtpg  14426  hash3tpde  14434  fprodle  15938  alzdvds  16266  algcvgblem  16523  lcmfunsnlem2lem2  16585  mndpsuppss  18668  lssne0  20833  dsmm0cl  21625  pmatcollpw2lem  22640  elcls  22936  cmpfi  23271  bwth  23273  1stccnp  23325  dissnlocfin  23392  trfil3  23751  isufil2  23771  bcth3  25207  rrxmvallem  25280  mdegleb  25945  tglowdim1i  28404  tglineintmo  28545  lmieu  28687  uhgrvd00  29438  wlkon2n0  29568  wwlks  29738  rusgrnumwwlks  29877  clwwlkneq0  29931  1to2vfriswmgr  30181  numclwwlk3lem2  30286  frgrregord013  30297  nmlno0lem  30695  lnon0  30700  nmlnop0iALT  31897  atom1d  32255  n0nsnel  32417  uniinn0  32452  nfpconfp  32529  funcnv5mpt  32565  suppiniseg  32582  xaddeq0  32649  pmtrcnel  33019  1arithidom  33481  fedgmullem2  33599  irredminply  33679  zarcls1  33832  bnj1533  34815  bnj1541  34819  bnj1279  34981  bnj1280  34983  bnj1311  34987  spthcycl  35089  nepss  35678  bj-ismooredr2  37071  nlpineqsn  37369  poimirlem31  37618  poimirlem32  37619  itg2addnclem2  37639  ftc1anc  37668  n0elqs  38287  lfl1  39036  lkreqN  39136  pmap0  39732  paddasslem17  39803  ltrnnid  40103  sticksstones1  42107  dffltz  42595  dflim5  43291  ntrneikb  44056  fzdifsuc2  45281  limclr  45626  liminflbuz2  45786  fourierdlem42  46120  fourierdlem76  46153  sge0cl  46352  meadjiunlem  46436  smfpimne2  46811  n0nsn2el  46999  oddprmne2  47689  usgrexmpl2trifr  48001  islininds2  48446  line2ylem  48713  line2xlem  48715  itsclc0xyqsol  48730  2itscp  48743  dmrnxp  48798  fdomne0  48811  oppcendc  48980