Definition df-2 12233

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 12225	. 2 class 2
2		c1 11028	. . 3 class 1
3		caddc 11030	. . 3 class +
4	2, 2, 3	co 7356	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12243  2re  12244  2cn  12245  0le2  12272  2pos  12273  1p1e2  12290  2p2e4  12300  2times  12301  1p2e3  12308  3p2e5  12316  4p2e6  12318  5p2e7  12321  6p2e8  12324  7p2e9  12326  1lt2  12336  nneo  12602  6p6e12  12707  7p5e12  12710  8p2e10  12713  8p4e12  12715  9p2e11  12720  9p3e12  12721  5t2e10  12733  eluz2b1  12858  x2times  13240  fztp  13523  fz12pr  13524  fztpval  13529  fzo12sn  13692  fzosplitpr  13721  sqval  14065  fac2  14230  faclbnd4lem1  14244  bcp1m1  14271  hashprg  14346  hashgt23el  14375  hashge2el2difr  14432  swrds2  14891  iseralt  15636  binom11  15786  climcndslem1  15803  climcndslem2  15804  bpoly1  16005  bpolydiflem  16008  bpoly3  16012  bpoly4  16013  ege2le3  16044  ef4p  16069  efgt1p2  16070  eirrlem  16160  odd2np1lem  16298  opoe  16321  bitsfzolem  16392  isprm3  16641  prmind2  16643  dvdsnprmd  16648  2mulprm  16651  pockthlem  16865  pockthg  16866  prmunb  16874  prmreclem2  16877  4sqlem19  16923  vdwlem12  16952  prmgaplem8  17018  2expltfac  17052  gsumpr12val  18646  mulg2  19048  psgnunilem2  19459  efgs1b  19700  efgredlemc  19709  lt6abl  19859  abvtrivd  20798  m2detleiblem2  22581  clmvs2  25049  cphipval  25198  pjthlem1  25392  ovolunlem1a  25451  ovolicc1  25471  vitalilem2  25564  itgcnlem  25745  dveflem  25934  coskpi  26475  ang180lem3  26763  tanatan  26871  cosatan  26873  atantayl2  26890  emcllem7  26953  basellem3  27034  basellem5  27036  basellem8  27039  issqf  27087  ppi2  27121  ppi3  27122  cht2  27123  ppieq0  27127  ppiublem2  27154  chpeq0  27159  chtub  27163  chpub  27171  mersenne  27178  perfectlem2  27181  bcp1ctr  27230  bclbnd  27231  bposlem1  27235  bposlem2  27236  bposlem6  27240  lgslem1  27248  lgsval2lem  27258  lgsdir2lem2  27277  lgsdir2lem3  27278  lgsdirprm  27282  lgseisen  27330  m1lgs  27339  rplogsumlem1  27435  rplogsumlem2  27436  dchrisum0flb  27461  dchrisum0re  27464  mulog2sumlem2  27486  pntrmax  27515  pntpbnd2  27538  pntibndlem2  27542  pntlemg  27549  pntlemr  27553  axlowdimlem13  29011  clwlkclwwlklem2a  30056  1wlkdlem1  30195  upgr3v3e3cycl  30238  upgr4cycl4dv4e  30243  numclwlk2lem2f1o  30437  ex-fl  30505  1p1e2apr1  30524  vc2OLD  30627  ipval2  30766  ip2i  30887  hv2times  31120  pjhthlem1  31450  ho2times  31878  stm1addi  32304  staddi  32305  stadd3i  32307  addltmulALT  32505  threehalves  32962  usgrgt2cycl  35300  subfacp1lem1  35349  subfacp1lem5  35354  subfacp1lem6  35355  sin2h  37919  tan2h  37921  poimirlem25  37954  poimirlem27  37956  itg2addnclem3  37982  aks4d1p1p7  42501  facp2  42570  sn-1ne2  42691  remul02  42825  sn-0tie0  42884  3cubeslem3r  43107  pell14qrgapw  43292  rmydioph  43430  rmxdioph  43432  expdiophlem1  43437  expdiophlem2  43438  expdioph  43439  relexp2  44092  stoweidlem14  46430  wallispilem3  46483  wallispi2lem2  46488  fourierswlem  46646  difmodm1lt  47801  perfectALTVlem2  48186  sbgoldbo  48251  nnsum3primes4  48252  nnsum3primesgbe  48256  nnlog2ge0lt1  49030  itcoval2  49128  ackval2  49146  ackval42  49160