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

Definition df-2 8930
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 8921 . 2  class  2
2 c1 8154 . . 3  class  1
3 caddc 8156 . . 3  class  +
42, 2, 3co 5356 . 2  class  ( 1  +  1 )
51, 4wceq 1518 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8939  2pos  8950  1p1e2  8961  2p2e4  8962  2timesi  8963  3p2e5  8975  4p2e6  8977  5p2e7  8980  6p2e8  8984  7p2e9  8987  8p2e10  8989  2nn  8996  1lt2  9005  halfpos  9058  nneo  9199  6p6e12  9270  7p5e12  9272  8p4e12  9276  9p2e11  9281  9p3e12  9282  eluz2b1  9384  x2times  9648  fztp  9862  fzprval  9865  fztpval  9866  sqval  10170  fac2  10257  faclbnd4lem1  10269  bcp1m1  10295  hashprg  10330  iseralt  10828  binom11  10956  climcndslem1  10971  climcndslem2  10972  ege2le3  11030  ef4p  11051  efgt1p2  11052  eirrlem  11134  odd2np1lem  11237  isprm3  11340  prmind2  11342  opoe  11436  pockthlem  11523  pockthg  11524  prmunb  11532  prmreclem2  11535  4sqlem19  11581  vdwlem12  11610  decexp2  11661  swrds2  12622  mulg2  12751  efgs1b  13220  efgredlemc  13227  lt6abl  13353  abvtrivd  13776  pjthlem1  16943  ovolunlem1a  16997  ovolicc1  17017  vitalilem2  17106  itgcnlem  17286  dveflem  17441  coskpi  17912  ang180lem3  18022  tanatan  18167  cosatan  18169  atantayl2  18186  emcllem7  18245  basellem3  18268  basellem5  18270  basellem8  18273  issqf  18322  ppi2  18356  ppi3  18357  cht2  18358  ppieq0  18362  ppiublem2  18384  chpeq0  18389  chtublem  18392  chtub  18393  chpub  18401  bcp1ctr  18452  bclbnd  18453  bposlem1  18457  bposlem2  18458  bposlem6  18462  lgslem1  18469  lgsval2lem  18479  lgsdir2lem2  18497  lgsdir2lem3  18498  lgsdirprm  18502  lgseisen  18526  m1lgs  18535  rplogsumlem1  18564  rplogsumlem2  18565  dchrisum0flb  18589  dchrisum0re  18592  ex-fl  18656  1p1e2apr1  18661  vc2  18934  ipval2  19103  ip2i  19229  hv2times  19463  pjhthlem1  19793  ho2times  20222  stm1addi  20648  staddi  20649  stadd3i  20651  addltmulALT  20849  subfacp1lem1  20874  subfacp1lem5  20879  subfacp1lem6  20880  vdgr1d  21058  konigsberg  21075  axlowdimlem4  21742  axlowdimlem13  21751  bPoly1  21955  bpolydiflem  21958  intset  23218  pell14qrgapw  23993  rmydioph  24139  rmxdioph  24141  expdiophlem1  24146  expdiophlem2  24147  expdioph  24148  psgnunilem2  24493
Copyright terms: Public domain