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 12280
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 12272 . 2 class 8
2 c7 12271 . . 3 class 7
3 c1 11108 . . 3 class 1
4 caddc 11110 . . 3 class +
52, 3, 4co 7402 . 2 class (7 + 1)
61, 5wceq 1533 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  12306  8re  12307  8cn  12308  8pos  12323  8m1e7  12344  7p1e8  12360  4p4e8  12366  5p3e8  12368  6p2e8  12370  7p2e9  12372  7lt8  12403  8p8e16  12762  9p8e17  12769  9p9e18  12770  8t8e64  12797  9t8e72  12804  log2ub  26821  3cubeslem3r  41975  rmydioph  42303
  Copyright terms: Public domain W3C validator