HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-2 9182
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
StepHypRef Expression
1 c2 9173 . 2  class  2
2 c1 8159 . . 3  class  1
3 caddc 8161 . . 3  class  +
42, 2, 3co 5360 . 2  class  ( 1  +  1 )
51, 4wceq 1520 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9191  2pos  9202  1p1e2  9213  2p2e4  9214  2times  9215  3p2e5  9227  4p2e6  9229  5p2e7  9232  6p2e8  9236  7p2e9  9239  8p2e10  9241  2nn  9248  1lt2  9257  nneo  9464  6p6e12  9544  7p5e12  9546  8p4e12  9550  9p2e11  9555  9p3e12  9556  eluz2b1  9658  x2times  9987  fztp  10204  fzprval  10207  fztpval  10208  sqval  10518  fac2  10648  faclbnd4lem1  10660  bcp1m1  10686  hashprg  10721  iseralt  11348  binom11  11478  climcndslem1  11493  climcndslem2  11494  ege2le3  11554  ef4p  11576  efgt1p2  11577  eirrlem  11665  odd2np1lem  11768  isprm3  11872  prmind2  11874  opoe  11969  pockthlem  12057  pockthg  12058  prmunb  12066  prmreclem2  12069  4sqlem19  12115  vdwlem12  12144  decexp2  12195  swrds2  13156  mulg2  13285  efgs1b  13754  efgredlemc  13763  lt6abl  13889  abvtrivd  14313  pjthlem1  17481  ovolunlem1a  17535  ovolicc1  17555  vitalilem2  17644  itgcnlem  17824  dveflem  17980  coskpi  18472  ang180lem3  18594  tanatan  18769  cosatan  18771  atantayl2  18788  emcllem7  18849  basellem3  18874  basellem5  18876  basellem8  18879  issqf  18928  ppi2  18962  ppi3  18963  cht2  18964  ppieq0  18968  ppiublem2  18996  chpeq0  19001  chtublem  19004  chtub  19005  chpub  19013  mersenne  19020  perfectlem2  19023  bcp1ctr  19072  bclbnd  19073  bposlem1  19077  bposlem2  19078  bposlem6  19082  lgslem1  19089  lgsval2lem  19099  lgsdir2lem2  19117  lgsdir2lem3  19118  lgsdirprm  19122  lgseisen  19146  m1lgs  19155  rplogsumlem1  19187  rplogsumlem2  19188  dchrisum0flb  19213  dchrisum0re  19216  mulog2sumlem2  19238  pntrmax  19267  pntpbnd2  19290  pntibndlem2  19294  pntlemg  19301  pntlemr  19305  ex-fl  19366  1p1e2apr1  19371  vc2  19644  ipval2  19813  ip2i  19939  hv2times  20173  pjhthlem1  20503  ho2times  20932  stm1addi  21358  staddi  21359  stadd3i  21361  addltmulALT  21559  subfacp1lem1  21584  subfacp1lem5  21589  subfacp1lem6  21590  vdgr1d  21768  konigsberg  21785  axlowdimlem4  22450  axlowdimlem13  22459  bPoly1  22663  bpolydiflem  22666  intset  23865  pell14qrgapw  24735  rmydioph  24881  rmxdioph  24883  expdiophlem1  24888  expdiophlem2  24889  expdioph  24890  psgnunilem2  25235
Copyright terms: Public domain