Definition df-2 12213

Description: Define the number 2. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-2	⊢ 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2

Step	Hyp	Ref	Expression
1		c2 12205	. 2 class 2
2		c1 11032	. . 3 class 1
3		caddc 11034	. . 3 class +
4	2, 2, 3	co 7361	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12223  2re  12224  2cn  12225  0le2  12252  2pos  12253  1p1e2  12270  2p2e4  12280  2times  12281  1p2e3  12288  3p2e5  12296  4p2e6  12298  5p2e7  12301  6p2e8  12304  7p2e9  12306  1lt2  12316  nneo  12581  6p6e12  12686  7p5e12  12689  8p2e10  12692  8p4e12  12694  9p2e11  12699  9p3e12  12700  5t2e10  12712  eluz2b1  12837  x2times  13219  fztp  13501  fz12pr  13502  fztpval  13507  fzo12sn  13669  fzosplitpr  13698  sqval  14042  fac2  14207  faclbnd4lem1  14221  bcp1m1  14248  hashprg  14323  hashgt23el  14352  hashge2el2difr  14409  swrds2  14868  iseralt  15613  binom11  15760  climcndslem1  15777  climcndslem2  15778  bpoly1  15979  bpolydiflem  15982  bpoly3  15986  bpoly4  15987  ege2le3  16018  ef4p  16043  efgt1p2  16044  eirrlem  16134  odd2np1lem  16272  opoe  16295  bitsfzolem  16366  isprm3  16615  prmind2  16617  dvdsnprmd  16622  2mulprm  16625  pockthlem  16838  pockthg  16839  prmunb  16847  prmreclem2  16850  4sqlem19  16896  vdwlem12  16925  prmgaplem8  16991  2expltfac  17025  gsumpr12val  18619  mulg2  19018  psgnunilem2  19429  efgs1b  19670  efgredlemc  19679  lt6abl  19829  abvtrivd  20770  m2detleiblem2  22577  clmvs2  25055  cphipval  25204  pjthlem1  25398  ovolunlem1a  25458  ovolicc1  25478  vitalilem2  25571  itgcnlem  25752  dveflem  25944  coskpi  26493  ang180lem3  26782  tanatan  26890  cosatan  26892  atantayl2  26909  emcllem7  26973  basellem3  27054  basellem5  27056  basellem8  27059  issqf  27107  ppi2  27141  ppi3  27142  cht2  27143  ppieq0  27147  ppiublem2  27175  chpeq0  27180  chtub  27184  chpub  27192  mersenne  27199  perfectlem2  27202  bcp1ctr  27251  bclbnd  27252  bposlem1  27256  bposlem2  27257  bposlem6  27261  lgslem1  27269  lgsval2lem  27279  lgsdir2lem2  27298  lgsdir2lem3  27299  lgsdirprm  27303  lgseisen  27351  m1lgs  27360  rplogsumlem1  27456  rplogsumlem2  27457  dchrisum0flb  27482  dchrisum0re  27485  mulog2sumlem2  27507  pntrmax  27536  pntpbnd2  27559  pntibndlem2  27563  pntlemg  27570  pntlemr  27574  axlowdimlem13  29032  clwlkclwwlklem2a  30078  1wlkdlem1  30217  upgr3v3e3cycl  30260  upgr4cycl4dv4e  30265  numclwlk2lem2f1o  30459  ex-fl  30527  1p1e2apr1  30546  vc2OLD  30648  ipval2  30787  ip2i  30908  hv2times  31141  pjhthlem1  31471  ho2times  31899  stm1addi  32325  staddi  32326  stadd3i  32328  addltmulALT  32526  threehalves  32999  usgrgt2cycl  35337  subfacp1lem1  35386  subfacp1lem5  35391  subfacp1lem6  35392  sin2h  37824  tan2h  37826  poimirlem25  37859  poimirlem27  37861  itg2addnclem3  37887  aks4d1p1p7  42407  facp2  42476  sn-1ne2  42598  remul02  42738  sn-0tie0  42784  3cubeslem3r  43007  pell14qrgapw  43196  rmydioph  43334  rmxdioph  43336  expdiophlem1  43341  expdiophlem2  43342  expdioph  43343  relexp2  43996  stoweidlem14  46335  wallispilem3  46388  wallispi2lem2  46393  fourierswlem  46551  difmodm1lt  47682  perfectALTVlem2  48045  sbgoldbo  48110  nnsum3primes4  48111  nnsum3primesgbe  48115  nnlog2ge0lt1  48889  itcoval2  48987  ackval2  49005  ackval42  49019