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

Definition df-7 8486
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 8478 . 2 class 7
2 c6 8477 . . 3 class 6
3 c1 7351 . . 3 class 1
4 caddc 7353 . . 3 class +
52, 3, 4co 5652 . 2 class (6 + 1)
61, 5wceq 1289 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  8505  7pos  8524  6p1e7  8554  4p3e7  8560  5p2e7  8562  6p2e8  8565  7nn  8582  6lt7  8600  7p7e14  8955  8p7e15  8961  9p7e16  8968  9p8e17  8969  7t7e49  8990  8t7e56  8996  9t7e63  9003
  Copyright terms: Public domain W3C validator