Theorem nne 2962

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 2959	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 360	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 227	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  neirr  2967  necon3bd  2972  necon1d  2980  necon4d  2982  necon4bid  3003  necon1bbii  3007  pm2.61ine  3041  ne3anior  3052  sbcne12  4380  raldifsnb  4764  tpprceq3  4772  tppreqb  4773  prneimg  4819  prnebg  4821  xpeq0  6157  xpcan  6174  xpcan2  6175  fndmdifeq0  7039  ftpg  7153  fnnfpeq0  7176  suppimacnv  8166  fnsuppres  8183  suppcoss  8199  ixp0  8925  isfin5-2  10370  zornn0g  10484  nn0n0n1ge2b  12568  fsuppmapnn0fiub0  14025  fsuppmapnn0ub  14027  mptnn0fsupp  14029  mptnn0fsuppr  14031  discr  14272  hashgt12el  14455  hashgt12el2  14456  hashtpg  14518  hash3tpde  14526  fprodle  16046  alzdvds  16373  algcvgblem  16630  lcmfunsnlem2lem2  16692  mndpsuppss  18818  lssne0  21072  dsmm0cl  21890  pmatcollpw2lem  22934  elcls  23230  cmpfi  23565  bwth  23567  1stccnp  23619  dissnlocfin  23686  trfil3  24045  isufil2  24065  bcth3  25490  rrxmvallem  25563  mdegleb  26221  tglowdim1i  28770  tglineintmo  28915  symquadprlnglem  28970  lmieu  29093  prlngsymquadlem  29213  uhgrvd00  29884  wlkon2n0  30014  wwlks  30184  rusgrnumwwlks  30326  clwwlkneq0  30380  1to2vfriswmgr  30630  numclwwlk3lem2  30735  frgrregord013  30746  nmlno0lem  31145  lnon0  31150  nmlnop0iALT  32347  atom1d  32705  n0nsnel  32861  uniinn0  32897  nfpconfp  32977  funcnv5mpt  33012  suppiniseg  33031  xaddeq0  33098  pmtrcnel  33409  1arithidom  33827  esplymhp  33958  fedgmullem2  34020  irredminply  34106  zarcls1  34259  bnj1533  35240  bnj1541  35244  bnj1279  35406  bnj1280  35408  bnj1311  35412  spthcycl  35621  nepss  36210  ttcwf2  37036  bj-ismooredr2  37752  nlpineqsn  38054  poimirlem31  38302  poimirlem32  38303  itg2addnclem2  38323  ftc1anc  38352  n0elqs  38981  suceldisj  39467  lfl1  39844  lkreqN  39944  pmap0  40539  paddasslem17  40610  ltrnnid  40910  sticksstones1  42913  dffltz  43366  dflim5  44056  ntrneikb  44820  fzdifsuc2  46029  limclr  46369  liminflbuz2  46529  fourierdlem42  46863  fourierdlem76  46896  sge0cl  47095  meadjiunlem  47179  smfpimne2  47554  chnerlem1  47598  n0nsn2el  47762  oddprmne2  48480  usgrexmpl2trifr  48802  islininds2  49264  line2ylem  49531  line2xlem  49533  itsclc0xyqsol  49548  2itscp  49561  dmrnxp  49615  fdomne0  49628  oppcendc  49796