Definition df-2 12326

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 12318	. 2 class 2
2		c1 11153	. . 3 class 1
3		caddc 11155	. . 3 class +
4	2, 2, 3	co 7430	. 2 class (1 + 1)
5	1, 4	wceq 1536	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12336  2re  12337  2cn  12338  0le2  12365  2pos  12366  1p1e2  12388  2p2e4  12398  2times  12399  1p2e3  12406  3p2e5  12414  4p2e6  12416  5p2e7  12419  6p2e8  12422  7p2e9  12424  1lt2  12434  nneo  12699  6p6e12  12804  7p5e12  12807  8p2e10  12810  8p4e12  12812  9p2e11  12817  9p3e12  12818  5t2e10  12830  eluz2b1  12958  x2times  13337  fztp  13616  fz12pr  13617  fztpval  13622  fzo12sn  13783  fzosplitpr  13811  sqval  14151  fac2  14314  faclbnd4lem1  14328  bcp1m1  14355  hashprg  14430  hashgt23el  14459  hashge2el2difr  14516  swrds2  14975  iseralt  15717  binom11  15864  climcndslem1  15881  climcndslem2  15882  bpoly1  16083  bpolydiflem  16086  bpoly3  16090  bpoly4  16091  ege2le3  16122  ef4p  16145  efgt1p2  16146  eirrlem  16236  odd2np1lem  16373  opoe  16396  bitsfzolem  16467  isprm3  16716  prmind2  16718  dvdsnprmd  16723  2mulprm  16726  pockthlem  16938  pockthg  16939  prmunb  16947  prmreclem2  16950  4sqlem19  16996  vdwlem12  17025  prmgaplem8  17091  decexp2  17108  2expltfac  17126  gsumpr12val  18714  mulg2  19113  psgnunilem2  19527  efgs1b  19768  efgredlemc  19777  lt6abl  19927  abvtrivd  20849  m2detleiblem2  22649  clmvs2  25140  cphipval  25290  pjthlem1  25484  ovolunlem1a  25544  ovolicc1  25564  vitalilem2  25657  itgcnlem  25839  dveflem  26031  coskpi  26579  ang180lem3  26868  tanatan  26976  cosatan  26978  atantayl2  26995  emcllem7  27059  basellem3  27140  basellem5  27142  basellem8  27145  issqf  27193  ppi2  27227  ppi3  27228  cht2  27229  ppieq0  27233  ppiublem2  27261  chpeq0  27266  chtub  27270  chpub  27278  mersenne  27285  perfectlem2  27288  bcp1ctr  27337  bclbnd  27338  bposlem1  27342  bposlem2  27343  bposlem6  27347  lgslem1  27355  lgsval2lem  27365  lgsdir2lem2  27384  lgsdir2lem3  27385  lgsdirprm  27389  lgseisen  27437  m1lgs  27446  rplogsumlem1  27542  rplogsumlem2  27543  dchrisum0flb  27568  dchrisum0re  27571  mulog2sumlem2  27593  pntrmax  27622  pntpbnd2  27645  pntibndlem2  27649  pntlemg  27656  pntlemr  27660  axlowdimlem13  28983  clwlkclwwlklem2a  30026  1wlkdlem1  30165  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  numclwlk2lem2f1o  30407  ex-fl  30475  1p1e2apr1  30494  vc2OLD  30596  ipval2  30735  ip2i  30856  hv2times  31089  pjhthlem1  31419  ho2times  31847  stm1addi  32273  staddi  32274  stadd3i  32276  addltmulALT  32474  threehalves  32881  usgrgt2cycl  35114  subfacp1lem1  35163  subfacp1lem5  35168  subfacp1lem6  35169  sin2h  37596  tan2h  37598  poimirlem25  37631  poimirlem27  37633  itg2addnclem3  37659  aks4d1p1p7  42055  facp2  42124  fac2xp3  42220  sn-1ne2  42278  remul02  42411  sn-0tie0  42445  3cubeslem3r  42674  pell14qrgapw  42863  rmydioph  43002  rmxdioph  43004  expdiophlem1  43009  expdiophlem2  43010  expdioph  43011  relexp2  43666  stoweidlem14  45969  wallispilem3  46022  wallispi2lem2  46027  fourierswlem  46185  perfectALTVlem2  47646  sbgoldbo  47711  nnsum3primes4  47712  nnsum3primesgbe  47716  difmodm1lt  48371  nnlog2ge0lt1  48415  itcoval2  48513  ackval2  48531  ackval42  48545