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 11275
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 11266 . 2 class 8
2 c7 11265 . . 3 class 7
3 c1 10127 . . 3 class 1
4 caddc 10129 . . 3 class +
52, 3, 4co 6811 . 2 class (7 + 1)
61, 5wceq 1630 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8re  11295  8pos  11311  8m1e7  11332  7p1e8  11347  4p4e8  11354  5p3e8  11356  6p2e8  11359  7p2e9  11362  8nn  11381  7lt8  11405  8p8e16  11808  9p8e17  11816  9p9e18  11817  8t8e64  11852  9t8e72  11859  log2ub  24873  lgsdir2lem1  25247  lgsdir2lem3  25249  rmydioph  38081
  Copyright terms: Public domain W3C validator