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 10760
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 10751 . 2 class 5
2 c4 10750 . . 3 class 4
3 c1 9625 . . 3 class 1
4 caddc 9627 . . 3 class +
52, 3, 4co 6363 . 2 class (4 + 1)
61, 5wceq 1468 1 wff 5 = (4 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  5re  10777  5pos  10796  4p1e5  10826  3p2e5  10832  4p2e6  10834  5p5e10  10840  5nn  10860  4lt5  10872  6p5e11  11191  7p5e12  11194  8p5e13  11199  8p7e15  11201  9p5e14  11206  9p6e15  11207  5t5e25  11217  6t5e30  11221  7t5e35  11226  8t5e40  11232  9t5e45  11239  ef01bndlem  14398  5prm  15241  lt6abl  17690  log2ublem3  24035  ppiublem2  24292  bclbnd  24369  bposlem6  24378  bposlem9  24381  lgsdir2lem3  24414  rmydioph  36109  expdiophlem2  36117  stoweidlem13  38309  5odd  39357
  Copyright terms: Public domain W3C validator