Definition df-2 12321

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 12313	. 2 class 2
2		c1 11150	. . 3 class 1
3		caddc 11152	. . 3 class +
4	2, 2, 3	co 7416	. 2 class (1 + 1)
5	1, 4	wceq 1534	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12331  2re  12332  2cn  12333  0le2  12360  2pos  12361  1p1e2  12383  2p2e4  12393  2times  12394  1p2e3  12401  3p2e5  12409  4p2e6  12411  5p2e7  12414  6p2e8  12417  7p2e9  12419  1lt2  12429  nneo  12692  6p6e12  12797  7p5e12  12800  8p2e10  12803  8p4e12  12805  9p2e11  12810  9p3e12  12811  5t2e10  12823  eluz2b1  12949  x2times  13326  fztp  13605  fz12pr  13606  fztpval  13611  fzo12sn  13763  fzosplitpr  13790  sqval  14128  fac2  14291  faclbnd4lem1  14305  bcp1m1  14332  hashprg  14407  hashgt23el  14436  hashge2el2difr  14495  swrds2  14944  iseralt  15684  binom11  15831  climcndslem1  15848  climcndslem2  15849  bpoly1  16048  bpolydiflem  16051  bpoly3  16055  bpoly4  16056  ege2le3  16087  ef4p  16110  efgt1p2  16111  eirrlem  16201  odd2np1lem  16337  opoe  16360  bitsfzolem  16429  isprm3  16679  prmind2  16681  dvdsnprmd  16686  2mulprm  16689  pockthlem  16902  pockthg  16903  prmunb  16911  prmreclem2  16914  4sqlem19  16960  vdwlem12  16989  prmgaplem8  17055  decexp2  17072  2expltfac  17090  gsumpr12val  18677  mulg2  19073  psgnunilem2  19489  efgs1b  19730  efgredlemc  19739  lt6abl  19889  abvtrivd  20807  m2detleiblem2  22618  clmvs2  25109  cphipval  25259  pjthlem1  25453  ovolunlem1a  25513  ovolicc1  25533  vitalilem2  25626  itgcnlem  25807  dveflem  25999  coskpi  26547  ang180lem3  26836  tanatan  26944  cosatan  26946  atantayl2  26963  emcllem7  27027  basellem3  27108  basellem5  27110  basellem8  27113  issqf  27161  ppi2  27195  ppi3  27196  cht2  27197  ppieq0  27201  ppiublem2  27229  chpeq0  27234  chtub  27238  chpub  27246  mersenne  27253  perfectlem2  27256  bcp1ctr  27305  bclbnd  27306  bposlem1  27310  bposlem2  27311  bposlem6  27315  lgslem1  27323  lgsval2lem  27333  lgsdir2lem2  27352  lgsdir2lem3  27353  lgsdirprm  27357  lgseisen  27405  m1lgs  27414  rplogsumlem1  27510  rplogsumlem2  27511  dchrisum0flb  27536  dchrisum0re  27539  mulog2sumlem2  27561  pntrmax  27590  pntpbnd2  27613  pntibndlem2  27617  pntlemg  27624  pntlemr  27628  axlowdimlem13  28885  clwlkclwwlklem2a  29928  1wlkdlem1  30067  upgr3v3e3cycl  30110  upgr4cycl4dv4e  30115  numclwlk2lem2f1o  30309  ex-fl  30377  1p1e2apr1  30396  vc2OLD  30498  ipval2  30637  ip2i  30758  hv2times  30991  pjhthlem1  31321  ho2times  31749  stm1addi  32175  staddi  32176  stadd3i  32178  addltmulALT  32376  threehalves  32779  usgrgt2cycl  34971  subfacp1lem1  35020  subfacp1lem5  35025  subfacp1lem6  35026  sin2h  37324  tan2h  37326  poimirlem25  37359  poimirlem27  37361  itg2addnclem3  37387  aks4d1p1p7  41786  facp2  41855  fac2xp3  41947  sn-1ne2  42004  remul02  42116  sn-0tie0  42150  3cubeslem3r  42381  pell14qrgapw  42570  rmydioph  42709  rmxdioph  42711  expdiophlem1  42716  expdiophlem2  42717  expdioph  42718  relexp2  43381  stoweidlem14  45671  wallispilem3  45724  wallispi2lem2  45729  fourierswlem  45887  perfectALTVlem2  47330  sbgoldbo  47395  nnsum3primes4  47396  nnsum3primesgbe  47400  difmodm1lt  47946  nnlog2ge0lt1  47990  itcoval2  48088  ackval2  48106  ackval42  48120