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 1570   ≠ 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  4373  raldifsnb  4759  tpprceq3  4767  tppreqb  4768  prneimg  4814  prnebg  4816  xpeq0  6152  xpcan  6169  xpcan2  6170  fndmdifeq0  7036  ftpg  7153  fnnfpeq0  7176  suppimacnv  8172  fnsuppres  8189  suppcoss  8205  ixp0  8938  isfin5-2  10393  zornn0g  10507  nn0n0n1ge2b  12597  fsuppmapnn0fiub0  14057  fsuppmapnn0ub  14059  mptnn0fsupp  14061  mptnn0fsuppr  14063  discr  14304  hashgt12el  14487  hashgt12el2  14488  hashtpg  14550  hash3tpde  14558  fprodle  16083  alzdvds  16410  algcvgblem  16667  lcmfunsnlem2lem2  16729  mndpsuppss  18872  lssne0  21135  dsmm0cl  21953  pmatcollpw2lem  23002  elcls  23298  cmpfi  23633  bwth  23635  1stccnp  23688  dissnlocfin  23755  trfil3  24114  isufil2  24134  bcth3  25559  rrxmvallem  25632  mdegleb  26289  tglowdim1i  28843  tglineintmo  28989  symquadprlnglem  29044  lmieu  29168  prlngsymquadlem  29320  uhgrvd00  29994  wlkon2n0  30124  spthcycl  30271  wwlks  30303  rusgrnumwwlks  30445  clwwlkneq0  30499  1to2vfriswmgr  30759  numclwwlk3lem2  30864  frgrregord013  30875  nmlno0lem  31274  lnon0  31279  nmlnop0iALT  32476  atom1d  32834  n0nsnel  32990  uniinn0  33026  nfpconfp  33105  funcnv5mpt  33140  suppiniseg  33158  xaddeq0  33224  pmtrcnel  33529  1arithidom  33947  esplymhp  34078  fedgmullem2  34140  irredminply  34226  zarcls1  34379  bnj1533  35361  bnj1541  35365  bnj1279  35527  bnj1280  35529  bnj1311  35533  nepss  36297  ttcwf2  37144  bj-ismooredr2  37860  nlpineqsn  38162  poimirlem31  38400  poimirlem32  38401  itg2addnclem2  38421  ftc1anc  38450  n0elqs  39080  suceldisj  39566  lfl1  39943  lkreqN  40043  pmap0  40638  paddasslem17  40709  ltrnnid  41009  sticksstones1  43012  dffltz  43480  dflim5  44170  ntrneikb  44934  fzdifsuc2  46143  limclr  46483  liminflbuz2  46643  fourierdlem42  46977  fourierdlem76  47010  sge0cl  47209  meadjiunlem  47293  smfpimne2  47668  chnerlem1  47710  n0nsn2el  47913  oddprmne2  48631  usgrexmpl2trifr  48953  islininds2  49414  line2ylem  49681  line2xlem  49683  itsclc0xyqsol  49698  2itscp  49711  dmrnxp  49765  fdomne0  49778  oppcendc  49944  veroquaddetzerod  50819