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 11045
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 11036 . 2 class 8
2 c7 11035 . . 3 class 7
3 c1 9897 . . 3 class 1
4 caddc 9899 . . 3 class +
52, 3, 4co 6615 . 2 class (7 + 1)
61, 5wceq 1480 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8re  11065  8pos  11081  8m1e7  11102  7p1e8  11117  4p4e8  11124  5p3e8  11126  6p2e8  11129  7p2e9  11132  8nn  11151  7lt8  11175  8p8e16  11578  9p8e17  11586  9p9e18  11587  8t8e64  11622  9t8e72  11629  log2ub  24610  lgsdir2lem1  24984  lgsdir2lem3  24986  rmydioph  37100
  Copyright terms: Public domain W3C validator