Theorem nne 2938

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 2935	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2	1	con2bii 358	. 2 ⊢ (𝐴 = 𝐵 ↔ ¬ 𝐴 ≠ 𝐵)
3	2	bicomi 225	1 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  neirr  2943  necon3bd  2948  necon1d  2956  necon4d  2958  necon4bid  2979  necon1bbii  2983  pm2.61ine  3017  ne3anior  3028  sbcne12  4343  raldifsnb  4729  tpprceq3  4737  tppreqb  4738  prneimg  4785  prnebg  4787  xpeq0  6111  xpcan  6127  xpcan2  6128  fndmdifeq0  6985  ftpg  7099  fnnfpeq0  7122  suppimacnv  8114  fnsuppres  8131  suppcoss  8147  ixp0  8869  isfin5-2  10304  zornn0g  10418  nn0n0n1ge2b  12497  fsuppmapnn0fiub0  13946  fsuppmapnn0ub  13948  mptnn0fsupp  13950  mptnn0fsuppr  13952  discr  14193  hashgt12el  14375  hashgt12el2  14376  hashtpg  14438  hash3tpde  14446  fprodle  15952  alzdvds  16280  algcvgblem  16537  lcmfunsnlem2lem2  16599  mndpsuppss  18724  lssne0  20941  dsmm0cl  21715  pmatcollpw2lem  22760  elcls  23056  cmpfi  23391  bwth  23393  1stccnp  23445  dissnlocfin  23512  trfil3  23871  isufil2  23891  bcth3  25316  rrxmvallem  25389  mdegleb  26047  tglowdim1i  28587  tglineintmo  28728  lmieu  28870  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  32639  nfpconfp  32724  funcnv5mpt  32759  suppiniseg  32778  xaddeq0  32845  pmtrcnel  33170  1arithidom  33620  esplymhp  33752  fedgmullem2  33814  irredminply  33900  zarcls1  34053  bnj1533  35034  bnj1541  35038  bnj1279  35200  bnj1280  35202  bnj1311  35206  spthcycl  35357  nepss  35946  ttcwf2  36753  bj-ismooredr2  37468  nlpineqsn  37770  poimirlem31  38018  poimirlem32  38019  itg2addnclem2  38039  ftc1anc  38068  n0elqs  38699  suceldisj  39185  lfl1  39562  lkreqN  39662  pmap0  40257  paddasslem17  40328  ltrnnid  40628  sticksstones1  42631  dffltz  43084  dflim5  43774  ntrneikb  44538  fzdifsuc2  45758  limclr  46098  liminflbuz2  46258  fourierdlem42  46592  fourierdlem76  46625  sge0cl  46824  meadjiunlem  46908  smfpimne2  47283  chnerlem1  47327  n0nsn2el  47488  oddprmne2  48206  usgrexmpl2trifr  48528  islininds2  48975  line2ylem  49242  line2xlem  49244  itsclc0xyqsol  49259  2itscp  49272  dmrnxp  49327  fdomne0  49340  oppcendc  49508