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

Definition df-8 10625
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 10616 . 2
2 c7 10615 . . 3
3 c1 9514 . . 3
4 caddc 9516 . . 3
52, 3, 4co 6296 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  8re  10645  8pos  10661  7p1e8  10690  4p4e8  10697  5p3e8  10699  6p2e8  10702  7p2e9  10705  8nn  10724  7lt8  10748  8p8e16  11065  9p8e17  11072  9p9e18  11073  8t8e64  11098  9t8e72  11105  log2ub  23280  lgsdir2lem1  23598  lgsdir2lem3  23600  rmydioph  30956
  Copyright terms: Public domain W3C validator