Definition df-2 11414

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 11406	. 2 class 2
2		c1 10253	. . 3 class 1
3		caddc 10255	. . 3 class +
4	2, 2, 3	co 6905	. 2 class (1 + 1)
5	1, 4	wceq 1656	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  11424  2re  11425  2cn  11426  0le2  11460  2pos  11461  1p1e2  11483  2p2e4  11493  2times  11494  1p2e3  11501  3p2e5  11509  4p2e6  11511  5p2e7  11514  6p2e8  11517  7p2e9  11519  1lt2  11529  nneo  11789  6p6e12  11897  7p5e12  11900  8p2e10  11903  8p4e12  11905  9p2e11  11910  9p3e12  11911  5t2e10  11923  eluz2b1  12042  x2times  12417  fztp  12690  fz12pr  12691  fzprval  12695  fztpval  12696  fzo12sn  12846  fzosplitpr  12872  sqval  13216  fac2  13359  faclbnd4lem1  13373  bcp1m1  13400  hashprg  13472  hashge2el2difr  13552  swrds2  14061  iseralt  14792  binom11  14938  climcndslem1  14955  climcndslem2  14956  bpoly1  15154  bpolydiflem  15157  bpoly3  15161  bpoly4  15162  ege2le3  15192  ef4p  15215  efgt1p2  15216  eirrlem  15306  odd2np1lem  15438  opoe  15461  bitsfzolem  15529  isprm3  15768  prmind2  15770  dvdsnprmd  15775  prmgt1  15781  pockthlem  15980  pockthg  15981  prmunb  15989  prmreclem2  15992  4sqlem19  16038  vdwlem12  16067  prmgaplem8  16133  decexp2  16150  2expltfac  16165  gsumpr12val  17635  mulg2  17904  psgnunilem2  18266  efgs1b  18500  efgredlemc  18510  lt6abl  18649  abvtrivd  19196  m2detleiblem2  20802  clmvs2  23263  cphipval  23411  pjthlem1  23605  ovolunlem1a  23662  ovolicc1  23682  vitalilem2  23775  itgcnlem  23955  dveflem  24141  coskpi  24672  ang180lem3  24951  tanatan  25059  cosatan  25061  atantayl2  25078  emcllem7  25141  basellem3  25222  basellem5  25224  basellem8  25227  issqf  25275  ppi2  25309  ppi3  25310  cht2  25311  ppieq0  25315  ppiublem2  25341  chpeq0  25346  chtub  25350  chpub  25358  mersenne  25365  perfectlem2  25368  bcp1ctr  25417  bclbnd  25418  bposlem1  25422  bposlem2  25423  bposlem6  25427  lgslem1  25435  lgsval2lem  25445  lgsdir2lem2  25464  lgsdir2lem3  25465  lgsdirprm  25469  lgseisen  25517  m1lgs  25526  rplogsumlem1  25586  rplogsumlem2  25587  dchrisum0flb  25612  dchrisum0re  25615  mulog2sumlem2  25637  pntrmax  25666  pntpbnd2  25689  pntibndlem2  25693  pntlemg  25700  pntlemr  25704  axlowdimlem4  26244  axlowdimlem13  26253  clwlkclwwlklem2a  27327  1wlkdlem1  27502  upgr3v3e3cycl  27545  upgr4cycl4dv4e  27550  numclwlk2lem2f1o  27771  numclwlk2lem2f1oOLD  27774  numclwlk2lem2f1oOLDOLD  27782  ex-fl  27851  1p1e2apr1  27869  vc2OLD  27967  ipval2  28106  ip2i  28227  hv2times  28462  pjhthlem1  28794  ho2times  29222  stm1addi  29648  staddi  29649  stadd3i  29651  addltmulALT  29849  threehalves  30157  subfacp1lem1  31696  subfacp1lem5  31701  subfacp1lem6  31702  sin2h  33935  tan2h  33937  poimirlem25  33971  poimirlem27  33973  itg2addnclem3  33999  pell14qrgapw  38277  rmydioph  38417  rmxdioph  38419  expdiophlem1  38424  expdiophlem2  38425  expdioph  38426  relexp2  38803  stoweidlem14  41018  wallispilem3  41071  wallispi2lem2  41076  fourierswlem  41234  perfectALTVlem2  42454  sbgoldbo  42498  nnsum3primes4  42499  nnsum3primesgbe  42503  difmodm1lt  43157  nnlog2ge0lt1  43200