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

Definition df-8 8984
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 8976 . 2 class 8
2 c7 8975 . . 3 class 7
3 c1 7812 . . 3 class 1
4 caddc 7814 . . 3 class +
52, 3, 4co 5875 . 2 class (7 + 1)
61, 5wceq 1353 1 wff 8 = (7 + 1)
Colors of variables: wff set class
This definition is referenced by:  8re  9004  8pos  9022  8m1e7  9044  7p1e8  9058  4p4e8  9064  5p3e8  9066  6p2e8  9068  7p2e9  9070  8nn  9086  7lt8  9109  8p8e16  9469  9p8e17  9476  9p9e18  9477  8t8e64  9504  9t8e72  9511
  Copyright terms: Public domain W3C validator