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 12335
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 12327 . 2 class 8
2 c7 12326 . . 3 class 7
3 c1 11156 . . 3 class 1
4 caddc 11158 . . 3 class +
52, 3, 4co 7431 . 2 class (7 + 1)
61, 5wceq 1540 1 wff 8 = (7 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  8nn  12361  8re  12362  8cn  12363  8pos  12378  8m1e7  12399  7p1e8  12415  4p4e8  12421  5p3e8  12423  6p2e8  12425  7p2e9  12427  7lt8  12458  8p8e16  12819  9p8e17  12826  9p9e18  12827  8t8e64  12854  9t8e72  12861  log2ub  26992  3cubeslem3r  42698  rmydioph  43026
  Copyright terms: Public domain W3C validator