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 12025
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 12017 . 2 class 8
2 c7 12016 . . 3 class 7
3 c1 10856 . . 3 class 1
4 caddc 10858 . . 3 class +
52, 3, 4co 7268 . 2 class (7 + 1)
61, 5wceq 1541 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  12051  8re  12052  8cn  12053  8pos  12068  8m1e7  12089  7p1e8  12105  4p4e8  12111  5p3e8  12113  6p2e8  12115  7p2e9  12117  7lt8  12148  8p8e16  12505  9p8e17  12512  9p9e18  12513  8t8e64  12540  9t8e72  12547  log2ub  26080  3cubeslem3r  40489  rmydioph  40816
  Copyright terms: Public domain W3C validator