Theorem nne 2942

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  neirr  2947  necon3bd  2952  necon1d  2960  necon4d  2962  necon3aiOLD  2964  necon4bid  2984  necon1bbii  2988  pm2.61ine  3023  ne3anior  3034  sbcne12  4421  raldifsnb  4801  tpprceq3  4809  tppreqb  4810  prneimg  4859  prnebg  4861  xpeq0  6182  xpcan  6198  xpcan2  6199  fndmdifeq0  7064  ftpg  7176  fnnfpeq0  7198  suppimacnv  8198  fnsuppres  8215  suppcoss  8231  ixp0  8970  isfin5-2  10429  zornn0g  10543  nn0n0n1ge2b  12593  fsuppmapnn0fiub0  14031  fsuppmapnn0ub  14033  mptnn0fsupp  14035  mptnn0fsuppr  14037  discr  14276  hashgt12el  14458  hashgt12el2  14459  hashtpg  14521  hash3tpde  14529  fprodle  16029  alzdvds  16354  algcvgblem  16611  lcmfunsnlem2lem2  16673  mndpsuppss  18791  lssne0  20967  dsmm0cl  21778  pmatcollpw2lem  22799  elcls  23097  cmpfi  23432  bwth  23434  1stccnp  23486  dissnlocfin  23553  trfil3  23912  isufil2  23932  bcth3  25379  rrxmvallem  25452  mdegleb  26118  tglowdim1i  28524  tglineintmo  28665  lmieu  28807  uhgrvd00  29567  wlkon2n0  29699  wwlks  29865  rusgrnumwwlks  30004  clwwlkneq0  30058  1to2vfriswmgr  30308  numclwwlk3lem2  30413  frgrregord013  30424  nmlno0lem  30822  lnon0  30827  nmlnop0iALT  32024  atom1d  32382  n0nsnel  32543  uniinn0  32571  nfpconfp  32649  funcnv5mpt  32685  suppiniseg  32701  xaddeq0  32764  pmtrcnel  33092  1arithidom  33545  fedgmullem2  33658  irredminply  33722  zarcls1  33830  bnj1533  34845  bnj1541  34849  bnj1279  35011  bnj1280  35013  bnj1311  35017  spthcycl  35114  nepss  35698  bj-ismooredr2  37093  nlpineqsn  37391  poimirlem31  37638  poimirlem32  37639  itg2addnclem2  37659  ftc1anc  37688  n0elqs  38308  lfl1  39052  lkreqN  39152  pmap0  39748  paddasslem17  39819  ltrnnid  40119  sticksstones1  42128  dffltz  42621  dflim5  43319  ntrneikb  44084  fzdifsuc2  45261  limclr  45611  liminflbuz2  45771  fourierdlem42  46105  fourierdlem76  46138  sge0cl  46337  meadjiunlem  46421  smfpimne2  46796  n0nsn2el  46975  oddprmne2  47640  usgrexmpl2trifr  47932  islininds2  48330  line2ylem  48601  line2xlem  48603  itsclc0xyqsol  48618  2itscp  48631  fdomne0  48680