Definition df-2 12241

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 12233	. 2 class 2
2		c1 11036	. . 3 class 1
3		caddc 11038	. . 3 class +
4	2, 2, 3	co 7364	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12251  2re  12252  2cn  12253  0le2  12280  2pos  12281  1p1e2  12298  2p2e4  12308  2times  12309  1p2e3  12316  3p2e5  12324  4p2e6  12326  5p2e7  12329  6p2e8  12332  7p2e9  12334  1lt2  12344  nneo  12610  6p6e12  12715  7p5e12  12718  8p2e10  12721  8p4e12  12723  9p2e11  12728  9p3e12  12729  5t2e10  12741  eluz2b1  12866  x2times  13248  fztp  13531  fz12pr  13532  fztpval  13537  fzo12sn  13700  fzosplitpr  13729  sqval  14073  fac2  14238  faclbnd4lem1  14252  bcp1m1  14279  hashprg  14354  hashgt23el  14383  hashge2el2difr  14440  swrds2  14899  iseralt  15644  binom11  15794  climcndslem1  15811  climcndslem2  15812  bpoly1  16013  bpolydiflem  16016  bpoly3  16020  bpoly4  16021  ege2le3  16052  ef4p  16077  efgt1p2  16078  eirrlem  16168  odd2np1lem  16306  opoe  16329  bitsfzolem  16400  isprm3  16649  prmind2  16651  dvdsnprmd  16656  2mulprm  16659  pockthlem  16873  pockthg  16874  prmunb  16882  prmreclem2  16885  4sqlem19  16931  vdwlem12  16960  prmgaplem8  17026  2expltfac  17060  gsumpr12val  18654  mulg2  19056  psgnunilem2  19467  efgs1b  19708  efgredlemc  19717  lt6abl  19867  abvtrivd  20806  m2detleiblem2  22590  clmvs2  25058  cphipval  25207  pjthlem1  25401  ovolunlem1a  25460  ovolicc1  25480  vitalilem2  25573  itgcnlem  25754  dveflem  25943  coskpi  26484  ang180lem3  26772  tanatan  26880  cosatan  26882  atantayl2  26899  emcllem7  26962  basellem3  27043  basellem5  27045  basellem8  27048  issqf  27096  ppi2  27130  ppi3  27131  cht2  27132  ppieq0  27136  ppiublem2  27163  chpeq0  27168  chtub  27172  chpub  27180  mersenne  27187  perfectlem2  27190  bcp1ctr  27239  bclbnd  27240  bposlem1  27244  bposlem2  27245  bposlem6  27249  lgslem1  27257  lgsval2lem  27267  lgsdir2lem2  27286  lgsdir2lem3  27287  lgsdirprm  27291  lgseisen  27339  m1lgs  27348  rplogsumlem1  27444  rplogsumlem2  27445  dchrisum0flb  27470  dchrisum0re  27473  mulog2sumlem2  27495  pntrmax  27524  pntpbnd2  27547  pntibndlem2  27551  pntlemg  27558  pntlemr  27562  axlowdimlem13  29020  clwlkclwwlklem2a  30065  1wlkdlem1  30204  upgr3v3e3cycl  30247  upgr4cycl4dv4e  30252  numclwlk2lem2f1o  30446  ex-fl  30514  1p1e2apr1  30533  vc2OLD  30636  ipval2  30775  ip2i  30896  hv2times  31129  pjhthlem1  31459  ho2times  31887  stm1addi  32313  staddi  32314  stadd3i  32316  addltmulALT  32514  threehalves  32971  usgrgt2cycl  35309  subfacp1lem1  35358  subfacp1lem5  35363  subfacp1lem6  35364  sin2h  37928  tan2h  37930  poimirlem25  37963  poimirlem27  37965  itg2addnclem3  37991  aks4d1p1p7  42510  facp2  42579  sn-1ne2  42700  remul02  42834  sn-0tie0  42893  3cubeslem3r  43116  pell14qrgapw  43301  rmydioph  43439  rmxdioph  43441  expdiophlem1  43446  expdiophlem2  43447  expdioph  43448  relexp2  44101  stoweidlem14  46439  wallispilem3  46492  wallispi2lem2  46497  fourierswlem  46655  difmodm1lt  47804  perfectALTVlem2  48189  sbgoldbo  48254  nnsum3primes4  48255  nnsum3primesgbe  48259  nnlog2ge0lt1  49033  itcoval2  49131  ackval2  49149  ackval42  49163