Definition df-2 12249

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 12241	. 2 class 2
2		c1 11069	. . 3 class 1
3		caddc 11071	. . 3 class +
4	2, 2, 3	co 7387	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12259  2re  12260  2cn  12261  0le2  12288  2pos  12289  1p1e2  12306  2p2e4  12316  2times  12317  1p2e3  12324  3p2e5  12332  4p2e6  12334  5p2e7  12337  6p2e8  12340  7p2e9  12342  1lt2  12352  nneo  12618  6p6e12  12723  7p5e12  12726  8p2e10  12729  8p4e12  12731  9p2e11  12736  9p3e12  12737  5t2e10  12749  eluz2b1  12878  x2times  13259  fztp  13541  fz12pr  13542  fztpval  13547  fzo12sn  13709  fzosplitpr  13737  sqval  14079  fac2  14244  faclbnd4lem1  14258  bcp1m1  14285  hashprg  14360  hashgt23el  14389  hashge2el2difr  14446  swrds2  14906  iseralt  15651  binom11  15798  climcndslem1  15815  climcndslem2  15816  bpoly1  16017  bpolydiflem  16020  bpoly3  16024  bpoly4  16025  ege2le3  16056  ef4p  16081  efgt1p2  16082  eirrlem  16172  odd2np1lem  16310  opoe  16333  bitsfzolem  16404  isprm3  16653  prmind2  16655  dvdsnprmd  16660  2mulprm  16663  pockthlem  16876  pockthg  16877  prmunb  16885  prmreclem2  16888  4sqlem19  16934  vdwlem12  16963  prmgaplem8  17029  2expltfac  17063  gsumpr12val  18616  mulg2  19015  psgnunilem2  19425  efgs1b  19666  efgredlemc  19675  lt6abl  19825  abvtrivd  20741  m2detleiblem2  22515  clmvs2  24994  cphipval  25143  pjthlem1  25337  ovolunlem1a  25397  ovolicc1  25417  vitalilem2  25510  itgcnlem  25691  dveflem  25883  coskpi  26432  ang180lem3  26721  tanatan  26829  cosatan  26831  atantayl2  26848  emcllem7  26912  basellem3  26993  basellem5  26995  basellem8  26998  issqf  27046  ppi2  27080  ppi3  27081  cht2  27082  ppieq0  27086  ppiublem2  27114  chpeq0  27119  chtub  27123  chpub  27131  mersenne  27138  perfectlem2  27141  bcp1ctr  27190  bclbnd  27191  bposlem1  27195  bposlem2  27196  bposlem6  27200  lgslem1  27208  lgsval2lem  27218  lgsdir2lem2  27237  lgsdir2lem3  27238  lgsdirprm  27242  lgseisen  27290  m1lgs  27299  rplogsumlem1  27395  rplogsumlem2  27396  dchrisum0flb  27421  dchrisum0re  27424  mulog2sumlem2  27446  pntrmax  27475  pntpbnd2  27498  pntibndlem2  27502  pntlemg  27509  pntlemr  27513  axlowdimlem13  28881  clwlkclwwlklem2a  29927  1wlkdlem1  30066  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  numclwlk2lem2f1o  30308  ex-fl  30376  1p1e2apr1  30395  vc2OLD  30497  ipval2  30636  ip2i  30757  hv2times  30990  pjhthlem1  31320  ho2times  31748  stm1addi  32174  staddi  32175  stadd3i  32177  addltmulALT  32375  threehalves  32835  usgrgt2cycl  35117  subfacp1lem1  35166  subfacp1lem5  35171  subfacp1lem6  35172  sin2h  37604  tan2h  37606  poimirlem25  37639  poimirlem27  37641  itg2addnclem3  37667  aks4d1p1p7  42062  facp2  42131  sn-1ne2  42253  remul02  42393  sn-0tie0  42439  3cubeslem3r  42675  pell14qrgapw  42864  rmydioph  43003  rmxdioph  43005  expdiophlem1  43010  expdiophlem2  43011  expdioph  43012  relexp2  43666  stoweidlem14  46012  wallispilem3  46065  wallispi2lem2  46070  fourierswlem  46228  difmodm1lt  47357  perfectALTVlem2  47720  sbgoldbo  47785  nnsum3primes4  47786  nnsum3primesgbe  47790  nnlog2ge0lt1  48552  itcoval2  48650  ackval2  48668  ackval42  48682