Theorem nne 2959

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  neirr  2964  necon3bd  2969  necon1d  2977  necon4d  2979  necon4bid  3000  necon1bbii  3004  pm2.61ine  3038  ne3anior  3049  sbcne12  4372  raldifsnb  4755  tpprceq3  4763  tppreqb  4764  prneimg  4808  prnebg  4810  xpeq0  6153  xpcan  6170  xpcan2  6171  fndmdifeq0  7048  ftpg  7165  fnnfpeq0  7187  suppimacnv  8198  fnsuppres  8215  suppcoss  8231  ixp0  8966  isfin5-2  10476  zornn0g  10590  nn0n0n1ge2b  12682  fsuppmapnn0fiub0  14143  fsuppmapnn0ub  14145  mptnn0fsupp  14147  mptnn0fsuppr  14149  discr  14391  hashgt12el  14574  hashgt12el2  14575  hashtpg  14637  hash3tpde  14645  fprodle  16172  alzdvds  16499  algcvgblem  16761  lcmfunsnlem2lem2  16823  mndpsuppss  18968  lssne0  21235  dsmm0cl  22055  pmatcollpw2lem  23104  elcls  23400  cmpfi  23735  bwth  23737  1stccnp  23790  dissnlocfin  23857  trfil3  24216  isufil2  24236  bcth3  25661  rrxmvallem  25734  mdegleb  26391  tglowdim1i  28973  tglineintmo  29119  symquadprlnglem  29174  lmieu  29298  prlngsymquadlem  29450  uhgrvd00  30124  wlkon2n0  30254  spthcycl  30401  wwlks  30433  rusgrnumwwlks  30575  clwwlkneq0  30629  1to2vfriswmgr  30889  numclwwlk3lem2  30994  frgrregord013  31005  nmlno0lem  31404  lnon0  31409  nmlnop0iALT  32606  atom1d  32964  n0nsnel  33162  uniinn0  33198  nfpconfp  33277  funcnv5mpt  33312  suppiniseg  33330  xaddeq0  33395  pmtrcnel  33700  1arithidom  34119  esplymhp  34250  fedgmullem2  34312  irredminply  34398  zarcls1  34551  bnj1533  35532  bnj1541  35536  bnj1279  35698  bnj1280  35700  bnj1311  35704  nepss  36579  ttcwf2  37409  bj-ismooredr2  38139  nlpineqsn  38440  poimirlem31  38678  poimirlem32  38679  itg2addnclem2  38699  ftc1anc  38728  n0elqs  39373  suceldisj  39859  lfl1  40236  lkreqN  40336  pmap0  40931  paddasslem17  41002  ltrnnid  41302  sticksstones1  43305  frlmnzcoordex  43761  dffltz  43779  dflim5  44440  ntrneikb  45203  fzdifsuc2  46434  limclr  46773  liminflbuz2  46933  fourierdlem42  47267  fourierdlem76  47300  sge0cl  47499  meadjiunlem  47583  smfpimne2  47958  chnerlem1  48000  n0nsn2el  48203  oddprmne2  48921  usgrexmpl2trifr  49243  islininds2  49704  line2ylem  49971  line2xlem  49973  itsclc0xyqsol  49988  2itscp  50001  dmrnxp  50056  fdomne0  50069  oppcendc  50240  veroquaddetzerod  51169