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 11366
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 11358 . 2 class 8
2 c7 11357 . . 3 class 7
3 c1 10218 . . 3 class 1
4 caddc 10220 . . 3 class +
52, 3, 4co 6870 . 2 class (7 + 1)
61, 5wceq 1637 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8re  11385  8pos  11400  8m1e7  11421  7p1e8  11436  4p4e8  11442  5p3e8  11444  6p2e8  11446  7p2e9  11448  8nn  11464  7lt8  11487  8p8e16  11841  9p8e17  11848  9p9e18  11849  8t8e64  11876  9t8e72  11883  log2ub  24886  lgsdir2lem1  25260  lgsdir2lem3  25262  rmydioph  38076
  Copyright terms: Public domain W3C validator