Theorem nne 2936

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  neirr  2941  necon3bd  2946  necon1d  2954  necon4d  2956  necon4bid  2977  necon1bbii  2981  pm2.61ine  3015  ne3anior  3026  sbcne12  4367  raldifsnb  4752  tpprceq3  4760  tppreqb  4761  prneimg  4810  prnebg  4812  xpeq0  6118  xpcan  6134  xpcan2  6135  fndmdifeq0  6989  ftpg  7101  fnnfpeq0  7124  suppimacnv  8116  fnsuppres  8133  suppcoss  8149  ixp0  8869  isfin5-2  10301  zornn0g  10415  nn0n0n1ge2b  12470  fsuppmapnn0fiub0  13916  fsuppmapnn0ub  13918  mptnn0fsupp  13920  mptnn0fsuppr  13922  discr  14163  hashgt12el  14345  hashgt12el2  14346  hashtpg  14408  hash3tpde  14416  fprodle  15919  alzdvds  16247  algcvgblem  16504  lcmfunsnlem2lem2  16566  mndpsuppss  18690  lssne0  20902  dsmm0cl  21695  pmatcollpw2lem  22721  elcls  23017  cmpfi  23352  bwth  23354  1stccnp  23406  dissnlocfin  23473  trfil3  23832  isufil2  23852  bcth3  25287  rrxmvallem  25360  mdegleb  26025  tglowdim1i  28573  tglineintmo  28714  lmieu  28856  uhgrvd00  29608  wlkon2n0  29738  wwlks  29908  rusgrnumwwlks  30050  clwwlkneq0  30104  1to2vfriswmgr  30354  numclwwlk3lem2  30459  frgrregord013  30470  nmlno0lem  30868  lnon0  30873  nmlnop0iALT  32070  atom1d  32428  n0nsnel  32590  uniinn0  32625  nfpconfp  32710  funcnv5mpt  32746  suppiniseg  32765  xaddeq0  32833  pmtrcnel  33171  1arithidom  33618  esplymhp  33726  fedgmullem2  33787  irredminply  33873  zarcls1  34026  bnj1533  35008  bnj1541  35012  bnj1279  35174  bnj1280  35176  bnj1311  35180  spthcycl  35323  nepss  35912  bj-ismooredr2  37315  nlpineqsn  37613  poimirlem31  37852  poimirlem32  37853  itg2addnclem2  37873  ftc1anc  37902  n0elqs  38525  lfl1  39330  lkreqN  39430  pmap0  40025  paddasslem17  40096  ltrnnid  40396  sticksstones1  42400  dffltz  42877  dflim5  43571  ntrneikb  44335  fzdifsuc2  45558  limclr  45899  liminflbuz2  46059  fourierdlem42  46393  fourierdlem76  46426  sge0cl  46625  meadjiunlem  46709  smfpimne2  47084  chnerlem1  47126  n0nsn2el  47271  oddprmne2  47961  usgrexmpl2trifr  48283  islininds2  48730  line2ylem  48997  line2xlem  48999  itsclc0xyqsol  49014  2itscp  49027  dmrnxp  49082  fdomne0  49095  oppcendc  49263