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 11695
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 11687 . 2 class 8
2 c7 11686 . . 3 class 7
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7145 . 2 class (7 + 1)
61, 5wceq 1528 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  11721  8re  11722  8cn  11723  8pos  11738  8m1e7  11759  7p1e8  11775  4p4e8  11781  5p3e8  11783  6p2e8  11785  7p2e9  11787  7lt8  11818  8p8e16  12173  9p8e17  12180  9p9e18  12181  8t8e64  12208  9t8e72  12215  log2ub  25455  3cubeslem3r  39164  rmydioph  39491
  Copyright terms: Public domain W3C validator