ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-8 GIF version

Definition df-8 8458
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 8450 . 2 class 8
2 c7 8449 . . 3 class 7
3 c1 7330 . . 3 class 1
4 caddc 7332 . . 3 class +
52, 3, 4co 5634 . 2 class (7 + 1)
61, 5wceq 1289 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  8478  8pos  8496  7p1e8  8525  4p4e8  8531  5p3e8  8533  6p2e8  8535  7p2e9  8537  8nn  8553  7lt8  8576  8p8e16  8931  9p8e17  8938  9p9e18  8939  8t8e64  8966  9t8e72  8973
  Copyright terms: Public domain W3C validator