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

Definition df-3 10043
Description: Define the number 3. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-3  |-  3  =  ( 2  +  1 )

Detailed syntax breakdown of Definition df-3
StepHypRef Expression
1 c3 10034 . 2  class  3
2 c2 10033 . . 3  class  2
3 c1 8975 . . 3  class  1
4 caddc 8977 . . 3  class  +
52, 3, 4co 6067 . 2  class  ( 2  +  1 )
61, 5wceq 1652 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  10055  3pos  10068  3m1e2  10080  3m1e2OLD  10081  2p2e4  10082  2p1e3  10087  3p3e6  10096  4p3e7  10098  5p3e8  10101  6p3e9  10105  7p3e10  10108  3t3e9  10113  3nn  10118  2lt3  10127  7p6e13  10420  8p3e11  10422  8p5e13  10424  9p3e12  10429  9p4e13  10430  4t3e12  10438  5t3e15  10440  6t3e18  10444  7t3e21  10449  8t3e24  10455  9t3e27  10462  fztpval  11091  fzo0to42pr  11169  cu2  11462  i3  11465  binom3  11483  fac3  11556  hashtpg  11674  sqrlem7  12037  ege2le3  12675  ef4p  12697  cos1bnd  12771  3prm  13079  13prm  13421  23prm  13424  43prm  13427  83prm  13428  163prm  13430  lt6abl  15487  vitalilem4  19486  iblcnlem1  19662  itgcnlem  19664  dveflem  19846  sincosq3sgn  20391  sincosq4sgn  20392  tangtx  20396  sincos6thpi  20406  ang180lem2  20635  mcubic  20670  cubic2  20671  binom4  20673  dquartlem2  20675  quart1  20679  quartlem1  20680  log2ublem3  20771  basellem5  20850  basellem8  20853  basellem9  20854  ppi3  20937  cht3  20939  ppiublem1  20969  ppiublem2  20970  ppiub  20971  chtub  20979  bclbnd  21047  bposlem2  21052  bposlem9  21059  lgsdir2lem3  21092  dchrvmasumiflem1  21178  mulog2sumlem2  21212  pntlemk  21283  pntlemo  21284  usgraexvlem  21397  constr3trllem3  21622  konigsberg  21692  ipval2  22186  stm1add3i  23733  stadd3i  23734  sinccvglem  25092  axlowdimlem3  25826  axlowdimlem13  25836  axlowdimlem16  25839  axlowdimlem17  25840  bpoly2  26046  bpoly4  26048  fsumcube  26049  mblfinlem2  26186  heiborlem6  26457  rabren3dioph  26808  rmydioph  27017  rmxdioph  27019  expdiophlem2  27025  expdioph  27026  stoweidlem26  27684
  Copyright terms: Public domain W3C validator