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

Definition df-8 10524
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 10515 . 2
2 c7 10514 . . 3
3 c1 9420 . . 3
4 caddc 9422 . . 3
52, 3, 4co 6222 . 2
61, 5wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  8re  10544  8pos  10560  7p1e8  10589  4p4e8  10596  5p3e8  10598  6p2e8  10601  7p2e9  10604  8nn  10623  7lt8  10647  8p8e16  10955  9p8e17  10962  9p9e18  10963  8t8e64  10988  9t8e72  10995  log2ub  22744  lgsdir2lem1  23062  lgsdir2lem3  23064  rmydioph  29823
  Copyright terms: Public domain W3C validator