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

Definition df-8 7977
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 7968 . 2 class 8
2 c7 7967 . . 3 class 7
3 c1 6888 . . 3 class 1
4 caddc 6890 . . 3 class +
52, 3, 4co 5512 . 2 class (7 + 1)
61, 5wceq 1243 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  7998  8pos  8017  7p1e8  8047  4p4e8  8054  5p3e8  8056  6p2e8  8059  7p2e9  8062  8nn  8081  7lt8  8105  8p8e16  8426  9p8e17  8433  9p9e18  8434  8t8e64  8459  9t8e72  8466
  Copyright terms: Public domain W3C validator