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 12332
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 12324 . 2 class 8
2 c7 12323 . . 3 class 7
3 c1 11153 . . 3 class 1
4 caddc 11155 . . 3 class +
52, 3, 4co 7430 . 2 class (7 + 1)
61, 5wceq 1536 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  12358  8re  12359  8cn  12360  8pos  12375  8m1e7  12396  7p1e8  12412  4p4e8  12418  5p3e8  12420  6p2e8  12422  7p2e9  12424  7lt8  12455  8p8e16  12816  9p8e17  12823  9p9e18  12824  8t8e64  12851  9t8e72  12858  log2ub  27006  3cubeslem3r  42674  rmydioph  43002
  Copyright terms: Public domain W3C validator