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  4356  raldifsnb  4740  tpprceq3  4748  tppreqb  4749  prneimg  4798  prnebg  4800  xpeq0  6119  xpcan  6135  xpcan2  6136  fndmdifeq0  6991  ftpg  7104  fnnfpeq0  7127  suppimacnv  8118  fnsuppres  8135  suppcoss  8151  ixp0  8873  isfin5-2  10307  zornn0g  10421  nn0n0n1ge2b  12500  fsuppmapnn0fiub0  13949  fsuppmapnn0ub  13951  mptnn0fsupp  13953  mptnn0fsuppr  13955  discr  14196  hashgt12el  14378  hashgt12el2  14379  hashtpg  14441  hash3tpde  14449  fprodle  15955  alzdvds  16283  algcvgblem  16540  lcmfunsnlem2lem2  16602  mndpsuppss  18727  lssne0  20940  dsmm0cl  21733  pmatcollpw2lem  22755  elcls  23051  cmpfi  23386  bwth  23388  1stccnp  23440  dissnlocfin  23507  trfil3  23866  isufil2  23886  bcth3  25311  rrxmvallem  25384  mdegleb  26042  tglowdim1i  28586  tglineintmo  28727  lmieu  28869  uhgrvd00  29621  wlkon2n0  29751  wwlks  29921  rusgrnumwwlks  30063  clwwlkneq0  30117  1to2vfriswmgr  30367  numclwwlk3lem2  30472  frgrregord013  30483  nmlno0lem  30882  lnon0  30887  nmlnop0iALT  32084  atom1d  32442  n0nsnel  32603  uniinn0  32638  nfpconfp  32723  funcnv5mpt  32758  suppiniseg  32777  xaddeq0  32844  pmtrcnel  33168  1arithidom  33615  esplymhp  33730  fedgmullem2  33793  irredminply  33879  zarcls1  34032  bnj1533  35013  bnj1541  35017  bnj1279  35179  bnj1280  35181  bnj1311  35185  spthcycl  35330  nepss  35919  ttcwf2  36726  bj-ismooredr2  37441  nlpineqsn  37741  poimirlem31  37989  poimirlem32  37990  itg2addnclem2  38010  ftc1anc  38039  n0elqs  38670  suceldisj  39156  lfl1  39533  lkreqN  39633  pmap0  40228  paddasslem17  40299  ltrnnid  40599  sticksstones1  42602  dffltz  43084  dflim5  43778  ntrneikb  44542  fzdifsuc2  45764  limclr  46104  liminflbuz2  46264  fourierdlem42  46598  fourierdlem76  46631  sge0cl  46830  meadjiunlem  46914  smfpimne2  47289  chnerlem1  47331  n0nsn2el  47488  oddprmne2  48206  usgrexmpl2trifr  48528  islininds2  48975  line2ylem  49242  line2xlem  49244  itsclc0xyqsol  49259  2itscp  49272  dmrnxp  49327  fdomne0  49340  oppcendc  49508