Definition df-2 12429

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 12421	. 2 class 2
2		c1 11225	. . 3 class 1
3		caddc 11227	. . 3 class +
4	2, 2, 3	co 7440	. 2 class (1 + 1)
5	1, 4	wceq 1570	1 wff 2 = (1 + 1)

This definition is used by:  2nn  12440  2re  12441  2cn  12442  0le2OLD  12470  2posOLD  12472  1p1e2  12490  2m1e1  12491  2p2e4  12501  2times  12502  1p2e3  12509  3p2e5  12517  4p2e6  12519  5p2e7  12522  6p2e8  12525  7p2e9  12527  1lt2  12539  nneo  12807  6p6e12  12917  7p5e12  12920  8p2e10  12923  8p4e12  12925  9p2e11  12930  9p3e12  12931  5t2e10  12943  eluz2b1  13070  x2times  13453  fztp  13738  fz12pr  13739  fztpval  13744  fzo12sn  13907  fzosplitpr  13936  sqval  14281  fac2  14447  faclbnd4lem1  14461  bcp1m1  14488  hashprg  14563  hashgt23el  14593  hashge2el2difr  14650  swrds2  15117  iseralt  15878  binom11  16027  climcndslem1  16044  climcndslem2  16045  bpoly1  16243  bpolydiflem  16246  bpoly3  16250  bpoly4  16251  ege2le3  16282  ef4p  16307  efgt1p2  16308  eirrlem  16398  odd2np1lem  16536  opoe  16559  bitsfzolem  16630  isprm3  16884  prmind2  16886  dvdsnprmd  16891  2mulprm  16894  pockthlem  17109  pockthg  17110  prmunb  17118  prmreclem2  17121  4sqlem19  17167  vdwlem12  17196  prmgaplem8  17262  2expltfac  17296  gsumpr12val  18904  mulg2  19319  psgnunilem2  19736  efgs1b  19977  efgredlemc  19986  lt6abl  20136  abvtrivd  21116  m2detleiblem2  22970  clmvs2  25442  cphipval  25591  pjthlem1  25785  ovolunlem1a  25844  ovolicc1  25864  vitalilem2  25957  itgcnlem  26137  dveflem  26326  coskpi  26878  ang180lem3  27166  tanatan  27274  cosatan  27276  atantayl2  27293  emcllem7  27356  basellem3  27437  basellem5  27439  basellem8  27442  issqf  27490  ppi2  27524  ppi3  27525  cht2  27526  ppieq0  27530  ppiublem2  27557  chpeq0  27562  chtub  27566  chpub  27574  mersenne  27581  perfectlem2  27584  bcp1ctr  27633  bclbnd  27634  bposlem1  27638  bposlem2  27639  bposlem6  27643  lgslem1  27651  lgsval2lem  27661  lgsdir2lem2  27680  lgsdir2lem3  27681  lgsdirprm  27685  lgseisen  27733  m1lgs  27742  rplogsumlem1  27838  rplogsumlem2  27839  dchrisum0flb  27864  dchrisum0re  27867  mulog2sumlem2  27889  pntrmax  27918  pntpbnd2  27941  pntibndlem2  27945  pntlemg  27952  pntlemr  27956  fltoprmlem2  28021  axlowdimlem13  29559  clwlkclwwlklem2a  30616  1wlkdlem1  30755  upgr3v3e3cycl  30808  upgr4cycl4dv4e  30813  numclwlk2lem2f1o  31007  ex-fl  31075  1p1e2apr1  31094  vc2OLD  31197  ipval2  31336  ip2i  31457  hv2times  31690  pjhthlem1  32020  ho2times  32448  stm1addi  32874  staddi  32875  stadd3i  32877  addltmulALT  33117  threehalves  33548  usgrgt2cycl  36065  subfacp1lem1  36110  subfacp1lem5  36115  subfacp1lem6  36116  sin2h  38724  tan2h  38726  poimirlem25  38754  poimirlem27  38756  itg2addnclem3  38782  aks4d1p1p7  43315  facp2  43384  sn-1ne2  43521  remul02  43647  sn-0tie0  43706  3cubeslem3r  43888  pell14qrgapw  44074  rmydioph  44212  rmxdioph  44214  expdiophlem1  44219  expdiophlem2  44220  expdioph  44221  relexp2  44867  stoweidlem14  47227  wallispilem3  47280  wallispi2lem2  47285  fourierswlem  47443  difmodm1lt  48638  perfectALTVlem2  49023  sbgoldbo  49088  nnsum3primes4  49089  nnsum3primesgbe  49093  nnlog2ge0lt1  49881  itcoval2  49979  ackval2  49997  ackval42  50011