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

Definition df-7 7976
Description: Define the number 7. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-7 7 = (6 + 1)

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 7967 . 2 class 7
2 c6 7966 . . 3 class 6
3 c1 6888 . . 3 class 1
4 caddc 6890 . . 3 class +
52, 3, 4co 5512 . 2 class (6 + 1)
61, 5wceq 1243 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  7996  7pos  8016  6p1e7  8046  4p3e7  8053  5p2e7  8055  6p2e8  8059  7nn  8080  6lt7  8099  7p7e14  8420  8p7e15  8425  9p7e16  8432  9p8e17  8433  7t7e49  8452  8t7e56  8458  9t7e63  8465
  Copyright terms: Public domain W3C validator