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

Definition df-7 8547
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 8539 . 2 class 7
2 c6 8538 . . 3 class 6
3 c1 7412 . . 3 class 1
4 caddc 7414 . . 3 class +
52, 3, 4co 5666 . 2 class (6 + 1)
61, 5wceq 1290 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  8566  7pos  8585  6p1e7  8615  4p3e7  8621  5p2e7  8623  6p2e8  8626  7nn  8643  6lt7  8661  7p7e14  9016  8p7e15  9022  9p7e16  9029  9p8e17  9030  7t7e49  9051  8t7e56  9057  9t7e63  9064
  Copyright terms: Public domain W3C validator