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

Definition df-5 10959
Description: Define the number 5. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-5 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 10950 . 2 class 5
2 c4 10949 . . 3 class 4
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (4 + 1)
61, 5wceq 1475 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  10976  5pos  10995  5m1e4  11016  4p1e5  11031  3p2e5  11037  4p2e6  11039  5p5e10OLD  11045  5nn  11065  4lt5  11077  5p5e10  11472  6p5e11  11476  6p5e11OLD  11477  7p5e12  11483  8p5e13  11491  8p7e15  11493  9p5e14  11499  9p6e15  11500  5t5e25  11515  5t5e25OLD  11516  6t5e30  11520  6t5e30OLD  11521  7t5e35  11527  8t5e40  11533  8t5e40OLD  11534  9t5e45  11542  fldiv4p1lem1div2  12498  ef01bndlem  14753  prm23lt5  15357  5prm  15653  lt6abl  18119  log2ublem3  24475  ppiublem2  24728  bclbnd  24805  bposlem6  24814  bposlem9  24817  lgsdir2lem3  24852  2lgslem3c  24923  2lgsoddprmlem3c  24937  ex-exp  26699  ex-fac  26700  ex-bc  26701  rmydioph  36599  expdiophlem2  36607  stoweidlem13  38906  fmtno5  40007  fmtnofac1  40020  31prm  40050  5odd  40157
  Copyright terms: Public domain W3C validator