Theorem nne 2960

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

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

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 2957

This theorem is used by:  neirr  2965  necon3bd  2970  necon1d  2978  necon4d  2980  necon4bid  3001  necon1bbii  3005  pm2.61ine  3039  ne3anior  3050  sbcne12  4373  raldifsnb  4759  tpprceq3  4767  tppreqb  4768  prneimg  4814  prnebg  4816  xpeq0  6151  xpcan  6168  xpcan2  6169  fndmdifeq0  7041  ftpg  7158  fnnfpeq0  7181  suppimacnv  8184  fnsuppres  8201  suppcoss  8217  ixp0  8952  isfin5-2  10462  zornn0g  10576  nn0n0n1ge2b  12668  fsuppmapnn0fiub0  14129  fsuppmapnn0ub  14131  mptnn0fsupp  14133  mptnn0fsuppr  14135  discr  14377  hashgt12el  14560  hashgt12el2  14561  hashtpg  14623  hash3tpde  14631  fprodle  16156  alzdvds  16483  algcvgblem  16745  lcmfunsnlem2lem2  16807  mndpsuppss  18952  lssne0  21219  dsmm0cl  22039  pmatcollpw2lem  23088  elcls  23384  cmpfi  23719  bwth  23721  1stccnp  23774  dissnlocfin  23841  trfil3  24200  isufil2  24220  bcth3  25645  rrxmvallem  25718  mdegleb  26375  tglowdim1i  28957  tglineintmo  29103  symquadprlnglem  29158  lmieu  29282  prlngsymquadlem  29434  uhgrvd00  30108  wlkon2n0  30238  spthcycl  30385  wwlks  30417  rusgrnumwwlks  30559  clwwlkneq0  30613  1to2vfriswmgr  30873  numclwwlk3lem2  30978  frgrregord013  30989  nmlno0lem  31388  lnon0  31393  nmlnop0iALT  32590  atom1d  32948  n0nsnel  33104  uniinn0  33140  nfpconfp  33219  funcnv5mpt  33254  suppiniseg  33272  xaddeq0  33338  pmtrcnel  33643  1arithidom  34062  esplymhp  34193  fedgmullem2  34255  irredminply  34341  zarcls1  34494  bnj1533  35475  bnj1541  35479  bnj1279  35641  bnj1280  35643  bnj1311  35647  nepss  36462  ttcwf2  37293  bj-ismooredr2  38011  nlpineqsn  38311  poimirlem31  38549  poimirlem32  38550  itg2addnclem2  38570  ftc1anc  38599  n0elqs  39244  suceldisj  39730  lfl1  40107  lkreqN  40207  pmap0  40802  paddasslem17  40873  ltrnnid  41173  sticksstones1  43176  frlmnzcoordex  43632  dffltz  43650  dflim5  44315  ntrneikb  45079  fzdifsuc2  46295  limclr  46634  liminflbuz2  46794  fourierdlem42  47128  fourierdlem76  47161  sge0cl  47360  meadjiunlem  47444  smfpimne2  47819  chnerlem1  47861  n0nsn2el  48064  oddprmne2  48782  usgrexmpl2trifr  49104  islininds2  49565  line2ylem  49832  line2xlem  49834  itsclc0xyqsol  49849  2itscp  49862  dmrnxp  49916  fdomne0  49929  oppcendc  50095  veroquaddetzerod  50955