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 11123
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 11114 . 2 class 8
2 c7 11113 . . 3 class 7
3 c1 9975 . . 3 class 1
4 caddc 9977 . . 3 class +
52, 3, 4co 6690 . 2 class (7 + 1)
61, 5wceq 1523 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8re  11143  8pos  11159  8m1e7  11180  7p1e8  11195  4p4e8  11202  5p3e8  11204  6p2e8  11207  7p2e9  11210  8nn  11229  7lt8  11253  8p8e16  11656  9p8e17  11664  9p9e18  11665  8t8e64  11700  9t8e72  11707  log2ub  24721  lgsdir2lem1  25095  lgsdir2lem3  25097  rmydioph  37898
  Copyright terms: Public domain W3C validator