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

Definition df-2 11697
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 11689 . 2 class 2
2 c1 10536 . . 3 class 1
3 caddc 10538 . . 3 class +
42, 2, 3co 7149 . 2 class (1 + 1)
51, 4wceq 1538 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2nn  11707  2re  11708  2cn  11709  0le2  11736  2pos  11737  1p1e2  11759  2p2e4  11769  2times  11770  1p2e3  11777  3p2e5  11785  4p2e6  11787  5p2e7  11790  6p2e8  11793  7p2e9  11795  1lt2  11805  nneo  12063  6p6e12  12169  7p5e12  12172  8p2e10  12175  8p4e12  12177  9p2e11  12182  9p3e12  12183  5t2e10  12195  eluz2b1  12316  x2times  12689  fztp  12967  fz12pr  12968  fztpval  12973  fzo12sn  13124  fzosplitpr  13150  sqval  13486  fac2  13644  faclbnd4lem1  13658  bcp1m1  13685  hashprg  13761  hashgt23el  13790  hashge2el2difr  13844  swrds2  14302  iseralt  15041  binom11  15187  climcndslem1  15204  climcndslem2  15205  bpoly1  15405  bpolydiflem  15408  bpoly3  15412  bpoly4  15413  ege2le3  15443  ef4p  15466  efgt1p2  15467  eirrlem  15557  odd2np1lem  15689  opoe  15712  bitsfzolem  15781  isprm3  16025  prmind2  16027  dvdsnprmd  16032  2mulprm  16035  pockthlem  16239  pockthg  16240  prmunb  16248  prmreclem2  16251  4sqlem19  16297  vdwlem12  16326  prmgaplem8  16392  decexp2  16409  2expltfac  16426  gsumpr12val  17899  mulg2  18237  psgnunilem2  18623  efgs1b  18862  efgredlemc  18871  lt6abl  19015  abvtrivd  19611  m2detleiblem2  21237  clmvs2  23702  cphipval  23850  pjthlem1  24044  ovolunlem1a  24103  ovolicc1  24123  vitalilem2  24216  itgcnlem  24396  dveflem  24585  coskpi  25118  ang180lem3  25400  tanatan  25508  cosatan  25510  atantayl2  25527  emcllem7  25590  basellem3  25671  basellem5  25673  basellem8  25676  issqf  25724  ppi2  25758  ppi3  25759  cht2  25760  ppieq0  25764  ppiublem2  25790  chpeq0  25795  chtub  25799  chpub  25807  mersenne  25814  perfectlem2  25817  bcp1ctr  25866  bclbnd  25867  bposlem1  25871  bposlem2  25872  bposlem6  25876  lgslem1  25884  lgsval2lem  25894  lgsdir2lem2  25913  lgsdir2lem3  25914  lgsdirprm  25918  lgseisen  25966  m1lgs  25975  rplogsumlem1  26071  rplogsumlem2  26072  dchrisum0flb  26097  dchrisum0re  26100  mulog2sumlem2  26122  pntrmax  26151  pntpbnd2  26174  pntibndlem2  26178  pntlemg  26185  pntlemr  26189  axlowdimlem13  26751  clwlkclwwlklem2a  27786  1wlkdlem1  27925  upgr3v3e3cycl  27968  upgr4cycl4dv4e  27973  numclwlk2lem2f1o  28167  ex-fl  28235  1p1e2apr1  28254  vc2OLD  28354  ipval2  28493  ip2i  28614  hv2times  28847  pjhthlem1  29177  ho2times  29605  stm1addi  30031  staddi  30032  stadd3i  30034  addltmulALT  30232  threehalves  30602  usgrgt2cycl  32434  subfacp1lem1  32483  subfacp1lem5  32488  subfacp1lem6  32489  sin2h  34992  tan2h  34994  poimirlem25  35027  poimirlem27  35029  itg2addnclem3  35055  facp2  39293  fac2xp3  39322  sn-1ne2  39396  remul02  39473  3cubeslem3r  39544  pell14qrgapw  39733  rmydioph  39871  rmxdioph  39873  expdiophlem1  39878  expdiophlem2  39879  expdioph  39880  relexp2  40294  stoweidlem14  42582  wallispilem3  42635  wallispi2lem2  42640  fourierswlem  42798  perfectALTVlem2  44166  sbgoldbo  44231  nnsum3primes4  44232  nnsum3primesgbe  44236  difmodm1lt  44862  nnlog2ge0lt1  44906  itcoval2  45004  ackval2  45022  ackval42  45036
  Copyright terms: Public domain W3C validator