MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2 Unicode version

Definition df-2 9229
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 9220 . 2  class  2
2 c1 8203 . . 3  class  1
3 caddc 8205 . . 3  class  +
42, 2, 3co 5404 . 2  class  ( 1  +  1 )
51, 4wceq 1531 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9240  2pos  9253  1p1e2  9265  2p2e4  9266  2times  9267  3p2e5  9279  4p2e6  9281  5p2e7  9284  6p2e8  9288  7p2e9  9291  8p2e10  9293  2nn  9301  1lt2  9310  nneo  9517  6p6e12  9597  7p5e12  9599  8p4e12  9603  9p2e11  9608  9p3e12  9609  eluz2b1  9711  x2times  10040  fztp  10257  fzprval  10260  fztpval  10261  sqval  10571  fac2  10701  faclbnd4lem1  10713  bcp1m1  10739  hashprg  10774  iseralt  11402  binom11  11532  climcndslem1  11547  climcndslem2  11548  ege2le3  11608  ef4p  11630  efgt1p2  11631  eirrlem  11719  odd2np1lem  11822  isprm3  11926  prmind2  11928  opoe  12023  pockthlem  12111  pockthg  12112  prmunb  12120  prmreclem2  12123  4sqlem19  12169  vdwlem12  12198  decexp2  12249  swrds2  13211  mulg2  13340  efgs1b  13809  efgredlemc  13818  lt6abl  13944  abvtrivd  14368  pjthlem1  17536  ovolunlem1a  17590  ovolicc1  17610  vitalilem2  17699  itgcnlem  17879  dveflem  18035  coskpi  18527  ang180lem3  18649  tanatan  18824  cosatan  18826  atantayl2  18843  emcllem7  18904  basellem3  18929  basellem5  18931  basellem8  18934  issqf  18983  ppi2  19017  ppi3  19018  cht2  19019  ppieq0  19023  ppiublem2  19051  chpeq0  19056  chtublem  19059  chtub  19060  chpub  19068  mersenne  19075  perfectlem2  19078  bcp1ctr  19127  bclbnd  19128  bposlem1  19132  bposlem2  19133  bposlem6  19137  lgslem1  19144  lgsval2lem  19154  lgsdir2lem2  19172  lgsdir2lem3  19173  lgsdirprm  19177  lgseisen  19201  m1lgs  19210  rplogsumlem1  19242  rplogsumlem2  19243  dchrisum0flb  19268  dchrisum0re  19271  mulog2sumlem2  19293  pntrmax  19322  pntpbnd2  19345  pntibndlem2  19349  pntlemg  19356  pntlemr  19360  ex-fl  19424  1p1e2apr1  19429  vc2  19702  ipval2  19871  ip2i  19997  hv2times  20231  pjhthlem1  20561  ho2times  20990  stm1addi  21416  staddi  21417  stadd3i  21419  addltmulALT  21617  subfacp1lem1  21642  subfacp1lem5  21647  subfacp1lem6  21648  vdgr1d  21826  konigsberg  21843  axlowdimlem4  22506  axlowdimlem13  22515  bPoly1  22719  bpolydiflem  22722  intset  23935  pell14qrgapw  24854  rmydioph  25000  rmxdioph  25002  expdiophlem1  25007  expdiophlem2  25008  expdioph  25009  psgnunilem2  25354
  Copyright terms: Public domain W3C validator