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

Definition df-8 8055
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 8046 . 2 class 8
2 c7 8045 . . 3 class 7
3 c1 6948 . . 3 class 1
4 caddc 6950 . . 3 class +
52, 3, 4co 5540 . 2 class (7 + 1)
61, 5wceq 1259 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  8075  8pos  8093  7p1e8  8122  4p4e8  8128  5p3e8  8130  6p2e8  8132  7p2e9  8134  8nn  8150  7lt8  8173  8p8e16  8512  9p8e17  8519  9p9e18  8520  8t8e64  8547  9t8e72  8554
  Copyright terms: Public domain W3C validator