Definition df-2 12272

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 12264	. 2 class 2
2		c1 11108	. . 3 class 1
3		caddc 11110	. . 3 class +
4	2, 2, 3	co 7406	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12282  2re  12283  2cn  12284  0le2  12311  2pos  12312  1p1e2  12334  2p2e4  12344  2times  12345  1p2e3  12352  3p2e5  12360  4p2e6  12362  5p2e7  12365  6p2e8  12368  7p2e9  12370  1lt2  12380  nneo  12643  6p6e12  12748  7p5e12  12751  8p2e10  12754  8p4e12  12756  9p2e11  12761  9p3e12  12762  5t2e10  12774  eluz2b1  12900  x2times  13275  fztp  13554  fz12pr  13555  fztpval  13560  fzo12sn  13712  fzosplitpr  13738  sqval  14077  fac2  14236  faclbnd4lem1  14250  bcp1m1  14277  hashprg  14352  hashgt23el  14381  hashge2el2difr  14439  swrds2  14888  iseralt  15628  binom11  15775  climcndslem1  15792  climcndslem2  15793  bpoly1  15992  bpolydiflem  15995  bpoly3  15999  bpoly4  16000  ege2le3  16030  ef4p  16053  efgt1p2  16054  eirrlem  16144  odd2np1lem  16280  opoe  16303  bitsfzolem  16372  isprm3  16617  prmind2  16619  dvdsnprmd  16624  2mulprm  16627  pockthlem  16835  pockthg  16836  prmunb  16844  prmreclem2  16847  4sqlem19  16893  vdwlem12  16922  prmgaplem8  16988  decexp2  17005  2expltfac  17023  gsumpr12val  18605  mulg2  18958  psgnunilem2  19358  efgs1b  19599  efgredlemc  19608  lt6abl  19758  abvtrivd  20441  m2detleiblem2  22122  clmvs2  24602  cphipval  24752  pjthlem1  24946  ovolunlem1a  25005  ovolicc1  25025  vitalilem2  25118  itgcnlem  25299  dveflem  25488  coskpi  26024  ang180lem3  26306  tanatan  26414  cosatan  26416  atantayl2  26433  emcllem7  26496  basellem3  26577  basellem5  26579  basellem8  26582  issqf  26630  ppi2  26664  ppi3  26665  cht2  26666  ppieq0  26670  ppiublem2  26696  chpeq0  26701  chtub  26705  chpub  26713  mersenne  26720  perfectlem2  26723  bcp1ctr  26772  bclbnd  26773  bposlem1  26777  bposlem2  26778  bposlem6  26782  lgslem1  26790  lgsval2lem  26800  lgsdir2lem2  26819  lgsdir2lem3  26820  lgsdirprm  26824  lgseisen  26872  m1lgs  26881  rplogsumlem1  26977  rplogsumlem2  26978  dchrisum0flb  27003  dchrisum0re  27006  mulog2sumlem2  27028  pntrmax  27057  pntpbnd2  27080  pntibndlem2  27084  pntlemg  27091  pntlemr  27095  axlowdimlem13  28202  clwlkclwwlklem2a  29241  1wlkdlem1  29380  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  numclwlk2lem2f1o  29622  ex-fl  29690  1p1e2apr1  29709  vc2OLD  29809  ipval2  29948  ip2i  30069  hv2times  30302  pjhthlem1  30632  ho2times  31060  stm1addi  31486  staddi  31487  stadd3i  31489  addltmulALT  31687  threehalves  32069  usgrgt2cycl  34110  subfacp1lem1  34159  subfacp1lem5  34164  subfacp1lem6  34165  sin2h  36467  tan2h  36469  poimirlem25  36502  poimirlem27  36504  itg2addnclem3  36530  aks4d1p1p7  40928  facp2  40948  fac2xp3  41009  sn-1ne2  41177  remul02  41275  sn-0tie0  41309  3cubeslem3r  41411  pell14qrgapw  41600  rmydioph  41739  rmxdioph  41741  expdiophlem1  41746  expdiophlem2  41747  expdioph  41748  relexp2  42414  stoweidlem14  44717  wallispilem3  44770  wallispi2lem2  44775  fourierswlem  44933  perfectALTVlem2  46377  sbgoldbo  46442  nnsum3primes4  46443  nnsum3primesgbe  46447  difmodm1lt  47162  nnlog2ge0lt1  47206  itcoval2  47304  ackval2  47322  ackval42  47336