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

Definition df-7 8054
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 8045 . 2 class 7
2 c6 8044 . . 3 class 6
3 c1 6948 . . 3 class 1
4 caddc 6950 . . 3 class +
52, 3, 4co 5540 . 2 class (6 + 1)
61, 5wceq 1259 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  8073  7pos  8092  6p1e7  8121  4p3e7  8127  5p2e7  8129  6p2e8  8132  7nn  8149  6lt7  8167  7p7e14  8505  8p7e15  8511  9p7e16  8518  9p8e17  8519  7t7e49  8540  8t7e56  8546  9t7e63  8553
  Copyright terms: Public domain W3C validator