Definition df-2 12356

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 12348	. 2 class 2
2		c1 11185	. . 3 class 1
3		caddc 11187	. . 3 class +
4	2, 2, 3	co 7448	. 2 class (1 + 1)
5	1, 4	wceq 1537	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12366  2re  12367  2cn  12368  0le2  12395  2pos  12396  1p1e2  12418  2p2e4  12428  2times  12429  1p2e3  12436  3p2e5  12444  4p2e6  12446  5p2e7  12449  6p2e8  12452  7p2e9  12454  1lt2  12464  nneo  12727  6p6e12  12832  7p5e12  12835  8p2e10  12838  8p4e12  12840  9p2e11  12845  9p3e12  12846  5t2e10  12858  eluz2b1  12984  x2times  13361  fztp  13640  fz12pr  13641  fztpval  13646  fzo12sn  13799  fzosplitpr  13826  sqval  14165  fac2  14328  faclbnd4lem1  14342  bcp1m1  14369  hashprg  14444  hashgt23el  14473  hashge2el2difr  14530  swrds2  14989  iseralt  15733  binom11  15880  climcndslem1  15897  climcndslem2  15898  bpoly1  16099  bpolydiflem  16102  bpoly3  16106  bpoly4  16107  ege2le3  16138  ef4p  16161  efgt1p2  16162  eirrlem  16252  odd2np1lem  16388  opoe  16411  bitsfzolem  16480  isprm3  16730  prmind2  16732  dvdsnprmd  16737  2mulprm  16740  pockthlem  16952  pockthg  16953  prmunb  16961  prmreclem2  16964  4sqlem19  17010  vdwlem12  17039  prmgaplem8  17105  decexp2  17122  2expltfac  17140  gsumpr12val  18727  mulg2  19123  psgnunilem2  19537  efgs1b  19778  efgredlemc  19787  lt6abl  19937  abvtrivd  20855  m2detleiblem2  22655  clmvs2  25146  cphipval  25296  pjthlem1  25490  ovolunlem1a  25550  ovolicc1  25570  vitalilem2  25663  itgcnlem  25845  dveflem  26037  coskpi  26583  ang180lem3  26872  tanatan  26980  cosatan  26982  atantayl2  26999  emcllem7  27063  basellem3  27144  basellem5  27146  basellem8  27149  issqf  27197  ppi2  27231  ppi3  27232  cht2  27233  ppieq0  27237  ppiublem2  27265  chpeq0  27270  chtub  27274  chpub  27282  mersenne  27289  perfectlem2  27292  bcp1ctr  27341  bclbnd  27342  bposlem1  27346  bposlem2  27347  bposlem6  27351  lgslem1  27359  lgsval2lem  27369  lgsdir2lem2  27388  lgsdir2lem3  27389  lgsdirprm  27393  lgseisen  27441  m1lgs  27450  rplogsumlem1  27546  rplogsumlem2  27547  dchrisum0flb  27572  dchrisum0re  27575  mulog2sumlem2  27597  pntrmax  27626  pntpbnd2  27649  pntibndlem2  27653  pntlemg  27660  pntlemr  27664  axlowdimlem13  28987  clwlkclwwlklem2a  30030  1wlkdlem1  30169  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  numclwlk2lem2f1o  30411  ex-fl  30479  1p1e2apr1  30498  vc2OLD  30600  ipval2  30739  ip2i  30860  hv2times  31093  pjhthlem1  31423  ho2times  31851  stm1addi  32277  staddi  32278  stadd3i  32280  addltmulALT  32478  threehalves  32879  usgrgt2cycl  35098  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  sin2h  37570  tan2h  37572  poimirlem25  37605  poimirlem27  37607  itg2addnclem3  37633  aks4d1p1p7  42031  facp2  42100  fac2xp3  42196  sn-1ne2  42254  remul02  42381  sn-0tie0  42415  3cubeslem3r  42643  pell14qrgapw  42832  rmydioph  42971  rmxdioph  42973  expdiophlem1  42978  expdiophlem2  42979  expdioph  42980  relexp2  43639  stoweidlem14  45935  wallispilem3  45988  wallispi2lem2  45993  fourierswlem  46151  perfectALTVlem2  47596  sbgoldbo  47661  nnsum3primes4  47662  nnsum3primesgbe  47666  difmodm1lt  48256  nnlog2ge0lt1  48300  itcoval2  48398  ackval2  48416  ackval42  48430