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  18674  lssne0  20889  dsmm0cl  21682  pmatcollpw2lem  22697  elcls  22993  cmpfi  23328  bwth  23330  1stccnp  23382  dissnlocfin  23449  trfil3  23808  isufil2  23828  bcth3  25264  rrxmvallem  25337  mdegleb  26002  tglowdim1i  28481  tglineintmo  28622  lmieu  28764  uhgrvd00  29515  wlkon2n0  29645  wwlks  29815  rusgrnumwwlks  29954  clwwlkneq0  30008  1to2vfriswmgr  30258  numclwwlk3lem2  30363  frgrregord013  30374  nmlno0lem  30772  lnon0  30777  nmlnop0iALT  31974  atom1d  32332  n0nsnel  32494  uniinn0  32529  nfpconfp  32606  funcnv5mpt  32642  suppiniseg  32659  xaddeq0  32726  pmtrcnel  33061  1arithidom  33501  fedgmullem2  33619  irredminply  33699  zarcls1  33852  bnj1533  34835  bnj1541  34839  bnj1279  35001  bnj1280  35003  bnj1311  35007  spthcycl  35109  nepss  35698  bj-ismooredr2  37091  nlpineqsn  37389  poimirlem31  37638  poimirlem32  37639  itg2addnclem2  37659  ftc1anc  37688  n0elqs  38307  lfl1  39056  lkreqN  39156  pmap0  39752  paddasslem17  39823  ltrnnid  40123  sticksstones1  42127  dffltz  42615  dflim5  43311  ntrneikb  44076  fzdifsuc2  45301  limclr  45646  liminflbuz2  45806  fourierdlem42  46140  fourierdlem76  46173  sge0cl  46372  meadjiunlem  46456  smfpimne2  46831  n0nsn2el  47019  oddprmne2  47709  usgrexmpl2trifr  48021  islininds2  48466  line2ylem  48733  line2xlem  48735  itsclc0xyqsol  48750  2itscp  48763  dmrnxp  48818  fdomne0  48831  oppcendc  49000