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

Definition df-2 8829
Description: Define the number 2.
Assertion
Ref Expression
df-2

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 8820 . 2
2 c1 8062 . . 3
3 caddc 8064 . . 3
42, 2, 3co 5296 . 2
51, 4wceq 1531 1
Colors of variables: wff set class
This definition is referenced by:  2re  8838  2pos  8849  1p1e2  8860  2p2e4  8861  2timesi  8862  3p2e5  8874  4p2e6  8876  5p2e7  8879  6p2e8  8883  7p2e9  8886  8p2e10  8888  2nn  8895  1lt2  8904  halfpos  8957  nneo  9096  6p6e12  9166  7p5e12  9168  8p4e12  9172  9p2e11  9177  9p3e12  9178  eluz2b1  9280  fztp  9645  fzprval  9648  fztpval  9649  sqval  9887  fac2  9972  faclbnd4lem1  9984  bcp1m1  10009  hashpr  10043  iseralt  10493  binom11  10616  climcndslem1  10631  climcndslem2  10632  ege2le3  10689  ef4p  10710  efgt1p2  10711  eirrlem  10793  odd2np1lem  10895  isprm3  10997  prmind2  10999  opoe  11063  pockthlem  11150  pockthg  11151  prmunb  11159  prmreclem2  11162  4sqlem19  11208  vdwlem12  11237  decexp2  11288  abvtrivd  12584  ovolunlem1a  14683  ovolicc1  14703  vitalilem2  14792  itgcnlem  14972  dveflem  15127  coskpi  15597  ang180lem3  15703  tanatan  15836  cosatan  15838  atantayl2  15855  emcllem7  15906  basellem3  15924  basellem5  15926  basellem8  15929  issqf  15958  ppi2  15988  ppi3  15989  cht2  15990  ppieq0  15994  ppiublem2  16010  chtublem  16013  chtub  16014  bcp1ctr  16019  bclbnd  16020  bposlem1  16024  bposlem2  16025  bposlem6  16029  lgslem1  16036  lgsval2lem  16046  lgsdir2lem2  16064  lgsdir2lem3  16065  lgsdirprm  16069  lgseisen  16087  m1lgs  16096  ex-fl  16169  1p1e2apr1  16174  vc2  16445  ipval2  16618  ip2i  16744  hv2times  16979  pjthlem1  17310  ho2times  17739  stm1addi  18164  staddi  18165  stadd3i  18167  addltmulALT  18365  subfacp1lem1  18390  subfacp1lem5  18395  subfacp1lem6  18396  vdgr1d  18578  konigsberg  18598  axlowdimlem4  19266  axlowdimlem13  19275  bPoly1  19479  bpolydiflem  19482  intset  20785  pell14qrgapw  21734  rmydioph  21884  rmxdioph  21886  expdiophlem1  21891  expdiophlem2  21892  expdioph  21893
Copyright terms: Public domain