MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-8 Unicode version

Definition df-8 10378
Description: Define the number 8. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-8

Detailed syntax breakdown of Definition df-8
StepHypRef Expression
1 c8 10369 . 2
2 c7 10368 . . 3
3 c1 9275 . . 3
4 caddc 9277 . . 3
52, 3, 4co 6086 . 2
61, 5wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  8re  10398  8pos  10414  7p1e8  10443  4p4e8  10450  5p3e8  10452  6p2e8  10455  7p2e9  10458  8nn  10477  7lt8  10501  8p8e16  10808  9p8e17  10815  9p9e18  10816  8t8e64  10841  9t8e72  10848  log2ub  22324  lgsdir2lem1  22642  lgsdir2lem3  22644  rmydioph  29334
  Copyright terms: Public domain W3C validator