Definition df-2 12225

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 12217	. 2 class 2
2		c1 11045	. . 3 class 1
3		caddc 11047	. . 3 class +
4	2, 2, 3	co 7369	. 2 class (1 + 1)
5	1, 4	wceq 1540	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12235  2re  12236  2cn  12237  0le2  12264  2pos  12265  1p1e2  12282  2p2e4  12292  2times  12293  1p2e3  12300  3p2e5  12308  4p2e6  12310  5p2e7  12313  6p2e8  12316  7p2e9  12318  1lt2  12328  nneo  12594  6p6e12  12699  7p5e12  12702  8p2e10  12705  8p4e12  12707  9p2e11  12712  9p3e12  12713  5t2e10  12725  eluz2b1  12854  x2times  13235  fztp  13517  fz12pr  13518  fztpval  13523  fzo12sn  13685  fzosplitpr  13713  sqval  14055  fac2  14220  faclbnd4lem1  14234  bcp1m1  14261  hashprg  14336  hashgt23el  14365  hashge2el2difr  14422  swrds2  14882  iseralt  15627  binom11  15774  climcndslem1  15791  climcndslem2  15792  bpoly1  15993  bpolydiflem  15996  bpoly3  16000  bpoly4  16001  ege2le3  16032  ef4p  16057  efgt1p2  16058  eirrlem  16148  odd2np1lem  16286  opoe  16309  bitsfzolem  16380  isprm3  16629  prmind2  16631  dvdsnprmd  16636  2mulprm  16639  pockthlem  16852  pockthg  16853  prmunb  16861  prmreclem2  16864  4sqlem19  16910  vdwlem12  16939  prmgaplem8  17005  2expltfac  17039  gsumpr12val  18592  mulg2  18991  psgnunilem2  19401  efgs1b  19642  efgredlemc  19651  lt6abl  19801  abvtrivd  20717  m2detleiblem2  22491  clmvs2  24970  cphipval  25119  pjthlem1  25313  ovolunlem1a  25373  ovolicc1  25393  vitalilem2  25486  itgcnlem  25667  dveflem  25859  coskpi  26408  ang180lem3  26697  tanatan  26805  cosatan  26807  atantayl2  26824  emcllem7  26888  basellem3  26969  basellem5  26971  basellem8  26974  issqf  27022  ppi2  27056  ppi3  27057  cht2  27058  ppieq0  27062  ppiublem2  27090  chpeq0  27095  chtub  27099  chpub  27107  mersenne  27114  perfectlem2  27117  bcp1ctr  27166  bclbnd  27167  bposlem1  27171  bposlem2  27172  bposlem6  27176  lgslem1  27184  lgsval2lem  27194  lgsdir2lem2  27213  lgsdir2lem3  27214  lgsdirprm  27218  lgseisen  27266  m1lgs  27275  rplogsumlem1  27371  rplogsumlem2  27372  dchrisum0flb  27397  dchrisum0re  27400  mulog2sumlem2  27422  pntrmax  27451  pntpbnd2  27474  pntibndlem2  27478  pntlemg  27485  pntlemr  27489  axlowdimlem13  28857  clwlkclwwlklem2a  29900  1wlkdlem1  30039  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  numclwlk2lem2f1o  30281  ex-fl  30349  1p1e2apr1  30368  vc2OLD  30470  ipval2  30609  ip2i  30730  hv2times  30963  pjhthlem1  31293  ho2times  31721  stm1addi  32147  staddi  32148  stadd3i  32150  addltmulALT  32348  threehalves  32808  usgrgt2cycl  35090  subfacp1lem1  35139  subfacp1lem5  35144  subfacp1lem6  35145  sin2h  37577  tan2h  37579  poimirlem25  37612  poimirlem27  37614  itg2addnclem3  37640  aks4d1p1p7  42035  facp2  42104  sn-1ne2  42226  remul02  42366  sn-0tie0  42412  3cubeslem3r  42648  pell14qrgapw  42837  rmydioph  42976  rmxdioph  42978  expdiophlem1  42983  expdiophlem2  42984  expdioph  42985  relexp2  43639  stoweidlem14  45985  wallispilem3  46038  wallispi2lem2  46043  fourierswlem  46201  difmodm1lt  47333  perfectALTVlem2  47696  sbgoldbo  47761  nnsum3primes4  47762  nnsum3primesgbe  47766  nnlog2ge0lt1  48528  itcoval2  48626  ackval2  48644  ackval42  48658