Theorem nne 2934

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

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

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 2931

This theorem is referenced by:  neirr  2939  necon3bd  2944  necon1d  2952  necon4d  2954  necon4bid  2975  necon1bbii  2979  pm2.61ine  3013  ne3anior  3024  sbcne12  4365  raldifsnb  4750  tpprceq3  4758  tppreqb  4759  prneimg  4808  prnebg  4810  xpeq0  6116  xpcan  6132  xpcan2  6133  fndmdifeq0  6987  ftpg  7099  fnnfpeq0  7122  suppimacnv  8114  fnsuppres  8131  suppcoss  8147  ixp0  8867  isfin5-2  10299  zornn0g  10413  nn0n0n1ge2b  12468  fsuppmapnn0fiub0  13914  fsuppmapnn0ub  13916  mptnn0fsupp  13918  mptnn0fsuppr  13920  discr  14161  hashgt12el  14343  hashgt12el2  14344  hashtpg  14406  hash3tpde  14414  fprodle  15917  alzdvds  16245  algcvgblem  16502  lcmfunsnlem2lem2  16564  mndpsuppss  18688  lssne0  20900  dsmm0cl  21693  pmatcollpw2lem  22719  elcls  23015  cmpfi  23350  bwth  23352  1stccnp  23404  dissnlocfin  23471  trfil3  23830  isufil2  23850  bcth3  25285  rrxmvallem  25358  mdegleb  26023  tglowdim1i  28522  tglineintmo  28663  lmieu  28805  uhgrvd00  29557  wlkon2n0  29687  wwlks  29857  rusgrnumwwlks  29999  clwwlkneq0  30053  1to2vfriswmgr  30303  numclwwlk3lem2  30408  frgrregord013  30419  nmlno0lem  30817  lnon0  30822  nmlnop0iALT  32019  atom1d  32377  n0nsnel  32539  uniinn0  32574  nfpconfp  32659  funcnv5mpt  32695  suppiniseg  32714  xaddeq0  32782  pmtrcnel  33120  1arithidom  33567  esplymhp  33675  fedgmullem2  33736  irredminply  33822  zarcls1  33975  bnj1533  34957  bnj1541  34961  bnj1279  35123  bnj1280  35125  bnj1311  35129  spthcycl  35272  nepss  35861  bj-ismooredr2  37254  nlpineqsn  37552  poimirlem31  37791  poimirlem32  37792  itg2addnclem2  37812  ftc1anc  37841  n0elqs  38464  lfl1  39269  lkreqN  39369  pmap0  39964  paddasslem17  40035  ltrnnid  40335  sticksstones1  42339  dffltz  42819  dflim5  43513  ntrneikb  44277  fzdifsuc2  45500  limclr  45841  liminflbuz2  46001  fourierdlem42  46335  fourierdlem76  46368  sge0cl  46567  meadjiunlem  46651  smfpimne2  47026  chnerlem1  47068  n0nsn2el  47213  oddprmne2  47903  usgrexmpl2trifr  48225  islininds2  48672  line2ylem  48939  line2xlem  48941  itsclc0xyqsol  48956  2itscp  48969  dmrnxp  49024  fdomne0  49037  oppcendc  49205