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 11506
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 11498 . 2 class 8
2 c7 11497 . . 3 class 7
3 c1 10332 . . 3 class 1
4 caddc 10334 . . 3 class +
52, 3, 4co 6974 . 2 class (7 + 1)
61, 5wceq 1507 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  11537  8re  11538  8cn  11539  8pos  11556  8m1e7  11577  7p1e8  11593  4p4e8  11599  5p3e8  11601  6p2e8  11603  7p2e9  11605  7lt8  11636  8p8e16  11996  9p8e17  12003  9p9e18  12004  8t8e64  12031  9t8e72  12038  log2ub  25223  rmydioph  38985
  Copyright terms: Public domain W3C validator