Definition df-2 12328

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 12320	. 2 class 2
2		c1 11126	. . 3 class 1
3		caddc 11128	. . 3 class +
4	2, 2, 3	co 7416	. 2 class (1 + 1)
5	1, 4	wceq 1570	1 wff 2 = (1 + 1)

This definition is used by:  2nn  12339  2re  12340  2cn  12341  0le2OLD  12369  2posOLD  12371  1p1e2  12389  2m1e1  12390  2p2e4  12400  2times  12401  1p2e3  12408  3p2e5  12416  4p2e6  12418  5p2e7  12421  6p2e8  12424  7p2e9  12426  1lt2  12438  nneo  12706  6p6e12  12816  7p5e12  12819  8p2e10  12822  8p4e12  12824  9p2e11  12829  9p3e12  12830  5t2e10  12842  eluz2b1  12969  x2times  13351  fztp  13635  fz12pr  13636  fztpval  13641  fzo12sn  13804  fzosplitpr  13833  sqval  14178  fac2  14343  faclbnd4lem1  14357  bcp1m1  14384  hashprg  14459  hashgt23el  14489  hashge2el2difr  14546  swrds2  15011  iseralt  15772  binom11  15921  climcndslem1  15938  climcndslem2  15939  bpoly1  16139  bpolydiflem  16142  bpoly3  16146  bpoly4  16147  ege2le3  16178  ef4p  16203  efgt1p2  16204  eirrlem  16294  odd2np1lem  16432  opoe  16455  bitsfzolem  16526  isprm3  16775  prmind2  16777  dvdsnprmd  16782  2mulprm  16785  pockthlem  16999  pockthg  17000  prmunb  17008  prmreclem2  17011  4sqlem19  17057  vdwlem12  17086  prmgaplem8  17152  2expltfac  17186  gsumpr12val  18791  mulg2  19205  psgnunilem2  19621  efgs1b  19862  efgredlemc  19871  lt6abl  20021  abvtrivd  20997  m2detleiblem2  22849  clmvs2  25321  cphipval  25470  pjthlem1  25664  ovolunlem1a  25723  ovolicc1  25743  vitalilem2  25836  itgcnlem  26017  dveflem  26206  coskpi  26756  ang180lem3  27044  tanatan  27152  cosatan  27154  atantayl2  27171  emcllem7  27234  basellem3  27315  basellem5  27317  basellem8  27320  issqf  27368  ppi2  27402  ppi3  27403  cht2  27404  ppieq0  27408  ppiublem2  27435  chpeq0  27440  chtub  27444  chpub  27452  mersenne  27459  perfectlem2  27462  bcp1ctr  27511  bclbnd  27512  bposlem1  27516  bposlem2  27517  bposlem6  27521  lgslem1  27529  lgsval2lem  27539  lgsdir2lem2  27558  lgsdir2lem3  27559  lgsdirprm  27563  lgseisen  27611  m1lgs  27620  rplogsumlem1  27716  rplogsumlem2  27717  dchrisum0flb  27742  dchrisum0re  27745  mulog2sumlem2  27767  pntrmax  27796  pntpbnd2  27819  pntibndlem2  27823  pntlemg  27830  pntlemr  27834  axlowdimlem13  29395  clwlkclwwlklem2a  30452  1wlkdlem1  30591  upgr3v3e3cycl  30644  upgr4cycl4dv4e  30649  numclwlk2lem2f1o  30843  ex-fl  30911  1p1e2apr1  30930  vc2OLD  31033  ipval2  31172  ip2i  31293  hv2times  31526  pjhthlem1  31856  ho2times  32284  stm1addi  32710  staddi  32711  stadd3i  32713  addltmulALT  32911  threehalves  33345  usgrgt2cycl  35708  subfacp1lem1  35743  subfacp1lem5  35748  subfacp1lem6  35749  sin2h  38349  tan2h  38351  poimirlem25  38379  poimirlem27  38381  itg2addnclem3  38407  aks4d1p1p7  42925  facp2  42994  sn-1ne2  43131  remul02  43265  sn-0tie0  43324  3cubeslem3r  43517  pell14qrgapw  43702  rmydioph  43840  rmxdioph  43842  expdiophlem1  43847  expdiophlem2  43848  expdioph  43849  relexp2  44502  stoweidlem14  46827  wallispilem3  46880  wallispi2lem2  46885  fourierswlem  47043  difmodm1lt  48238  perfectALTVlem2  48623  sbgoldbo  48688  nnsum3primes4  48689  nnsum3primesgbe  48693  nnlog2ge0lt1  49481  itcoval2  49579  ackval2  49597  ackval42  49611