Definition df-2 12282

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 12274	. 2 class 2
2		c1 11076	. . 3 class 1
3		caddc 11078	. . 3 class +
4	2, 2, 3	co 7398	. 2 class (1 + 1)
5	1, 4	wceq 1562	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12293  2re  12294  2cn  12295  0le2OLD  12323  2posOLD  12325  1p1e2  12343  2m1e1  12344  2p2e4  12354  2times  12355  1p2e3  12362  3p2e5  12370  4p2e6  12372  5p2e7  12375  6p2e8  12378  7p2e9  12380  1lt2  12392  nneo  12659  6p6e12  12769  7p5e12  12772  8p2e10  12775  8p4e12  12777  9p2e11  12782  9p3e12  12783  5t2e10  12795  eluz2b1  12922  x2times  13304  fztp  13587  fz12pr  13588  fztpval  13593  fzo12sn  13756  fzosplitpr  13785  sqval  14129  fac2  14294  faclbnd4lem1  14308  bcp1m1  14335  hashprg  14410  hashgt23el  14439  hashge2el2difr  14496  swrds2  14955  iseralt  15714  binom11  15864  climcndslem1  15881  climcndslem2  15882  bpoly1  16083  bpolydiflem  16086  bpoly3  16090  bpoly4  16091  ege2le3  16122  ef4p  16147  efgt1p2  16148  eirrlem  16238  odd2np1lem  16376  opoe  16399  bitsfzolem  16470  isprm3  16719  prmind2  16721  dvdsnprmd  16726  2mulprm  16729  pockthlem  16943  pockthg  16944  prmunb  16952  prmreclem2  16955  4sqlem19  17001  vdwlem12  17030  prmgaplem8  17096  2expltfac  17130  gsumpr12val  18725  mulg2  19127  psgnunilem2  19537  efgs1b  19778  efgredlemc  19787  lt6abl  19937  abvtrivd  20883  m2detleiblem2  22690  clmvs2  25158  cphipval  25307  pjthlem1  25501  ovolunlem1a  25560  ovolicc1  25580  vitalilem2  25673  itgcnlem  25854  dveflem  26043  coskpi  26590  ang180lem3  26878  tanatan  26986  cosatan  26988  atantayl2  27005  emcllem7  27068  basellem3  27149  basellem5  27151  basellem8  27154  issqf  27202  ppi2  27236  ppi3  27237  cht2  27238  ppieq0  27242  ppiublem2  27269  chpeq0  27274  chtub  27278  chpub  27286  mersenne  27293  perfectlem2  27296  bcp1ctr  27345  bclbnd  27346  bposlem1  27350  bposlem2  27351  bposlem6  27355  lgslem1  27363  lgsval2lem  27373  lgsdir2lem2  27392  lgsdir2lem3  27393  lgsdirprm  27397  lgseisen  27445  m1lgs  27454  rplogsumlem1  27550  rplogsumlem2  27551  dchrisum0flb  27576  dchrisum0re  27579  mulog2sumlem2  27601  pntrmax  27630  pntpbnd2  27653  pntibndlem2  27657  pntlemg  27664  pntlemr  27668  axlowdimlem13  29157  clwlkclwwlklem2a  30202  1wlkdlem1  30341  upgr3v3e3cycl  30384  upgr4cycl4dv4e  30389  numclwlk2lem2f1o  30583  ex-fl  30651  1p1e2apr1  30670  vc2OLD  30773  ipval2  30912  ip2i  31033  hv2times  31266  pjhthlem1  31596  ho2times  32024  stm1addi  32450  staddi  32451  stadd3i  32453  addltmulALT  32651  threehalves  33094  usgrgt2cycl  35485  subfacp1lem1  35534  subfacp1lem5  35539  subfacp1lem6  35540  sin2h  38114  tan2h  38116  poimirlem25  38149  poimirlem27  38151  itg2addnclem3  38177  aks4d1p1p7  42696  facp2  42765  sn-1ne2  42885  remul02  43019  sn-0tie0  43078  3cubeslem3r  43273  pell14qrgapw  43458  rmydioph  43596  rmxdioph  43598  expdiophlem1  43603  expdiophlem2  43604  expdioph  43605  relexp2  44258  stoweidlem14  46593  wallispilem3  46646  wallispi2lem2  46651  fourierswlem  46809  difmodm1lt  47964  perfectALTVlem2  48349  sbgoldbo  48414  nnsum3primes4  48415  nnsum3primesgbe  48419  nnlog2ge0lt1  49193  itcoval2  49291  ackval2  49309  ackval42  49323