Definition df-2 12405

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 12397	. 2 class 2
2		c1 11201	. . 3 class 1
3		caddc 11203	. . 3 class +
4	2, 2, 3	co 7420	. 2 class (1 + 1)
5	1, 4	wceq 1569	1 wff 2 = (1 + 1)

This definition is used by:  2nn  12416  2re  12417  2cn  12418  0le2OLD  12446  2posOLD  12448  1p1e2  12466  2m1e1  12467  2p2e4  12477  2times  12478  1p2e3  12485  3p2e5  12493  4p2e6  12495  5p2e7  12498  6p2e8  12501  7p2e9  12503  1lt2  12515  nneo  12783  6p6e12  12893  7p5e12  12896  8p2e10  12899  8p4e12  12901  9p2e11  12906  9p3e12  12907  5t2e10  12919  eluz2b1  13046  x2times  13429  fztp  13714  fz12pr  13715  fztpval  13720  fzo12sn  13883  fzosplitpr  13912  sqval  14257  fac2  14423  faclbnd4lem1  14437  bcp1m1  14464  hashprg  14539  hashgt23el  14569  hashge2el2difr  14626  swrds2  15091  iseralt  15852  binom11  16001  climcndslem1  16018  climcndslem2  16019  bpoly1  16217  bpolydiflem  16220  bpoly3  16224  bpoly4  16225  ege2le3  16256  ef4p  16281  efgt1p2  16282  eirrlem  16372  odd2np1lem  16510  opoe  16533  bitsfzolem  16604  isprm3  16858  prmind2  16860  dvdsnprmd  16865  2mulprm  16868  pockthlem  17083  pockthg  17084  prmunb  17092  prmreclem2  17095  4sqlem19  17141  vdwlem12  17170  prmgaplem8  17236  2expltfac  17270  gsumpr12val  18878  mulg2  19293  psgnunilem2  19709  efgs1b  19950  efgredlemc  19959  lt6abl  20109  abvtrivd  21089  m2detleiblem2  22943  clmvs2  25415  cphipval  25564  pjthlem1  25758  ovolunlem1a  25817  ovolicc1  25837  vitalilem2  25930  itgcnlem  26110  dveflem  26299  coskpi  26851  ang180lem3  27139  tanatan  27247  cosatan  27249  atantayl2  27266  emcllem7  27329  basellem3  27410  basellem5  27412  basellem8  27415  issqf  27463  ppi2  27497  ppi3  27498  cht2  27499  ppieq0  27503  ppiublem2  27530  chpeq0  27535  chtub  27539  chpub  27547  mersenne  27554  perfectlem2  27557  bcp1ctr  27606  bclbnd  27607  bposlem1  27611  bposlem2  27612  bposlem6  27616  lgslem1  27624  lgsval2lem  27634  lgsdir2lem2  27653  lgsdir2lem3  27654  lgsdirprm  27658  lgseisen  27706  m1lgs  27715  rplogsumlem1  27811  rplogsumlem2  27812  dchrisum0flb  27837  dchrisum0re  27840  mulog2sumlem2  27862  pntrmax  27891  pntpbnd2  27914  pntibndlem2  27918  pntlemg  27925  pntlemr  27929  fltoprmlem2  27994  axlowdimlem13  29532  clwlkclwwlklem2a  30589  1wlkdlem1  30728  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  numclwlk2lem2f1o  30980  ex-fl  31048  1p1e2apr1  31067  vc2OLD  31170  ipval2  31309  ip2i  31430  hv2times  31663  pjhthlem1  31993  ho2times  32421  stm1addi  32847  staddi  32848  stadd3i  32850  addltmulALT  33090  threehalves  33523  usgrgt2cycl  35951  subfacp1lem1  35986  subfacp1lem5  35991  subfacp1lem6  35992  sin2h  38576  tan2h  38578  poimirlem25  38606  poimirlem27  38608  itg2addnclem3  38634  aks4d1p1p7  43167  facp2  43236  sn-1ne2  43373  remul02  43499  sn-0tie0  43558  3cubeslem3r  43740  pell14qrgapw  43925  rmydioph  44063  rmxdioph  44065  expdiophlem1  44070  expdiophlem2  44071  expdioph  44072  relexp2  44719  stoweidlem14  47066  wallispilem3  47119  wallispi2lem2  47124  fourierswlem  47282  difmodm1lt  48477  perfectALTVlem2  48862  sbgoldbo  48927  nnsum3primes4  48928  nnsum3primesgbe  48932  nnlog2ge0lt1  49720  itcoval2  49818  ackval2  49836  ackval42  49850