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

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

Detailed syntax breakdown of Definition df-8
StepHypRef Expression
1 c8 10923 . 2 class 8
2 c7 10922 . . 3 class 7
3 c1 9793 . . 3 class 1
4 caddc 9795 . . 3 class +
52, 3, 4co 6527 . 2 class (7 + 1)
61, 5wceq 1474 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8re  10952  8pos  10968  8m1e7  10989  7p1e8  11004  4p4e8  11011  5p3e8  11013  6p2e8  11016  7p2e9  11019  8nn  11038  7lt8  11062  8p8e16  11450  9p8e17  11458  9p9e18  11459  8t8e64  11494  9t8e72  11501  log2ub  24393  lgsdir2lem1  24767  lgsdir2lem3  24769  rmydioph  36395
  Copyright terms: Public domain W3C validator