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

Definition df-7 8791
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 8783 . 2 class 7
2 c6 8782 . . 3 class 6
3 c1 7628 . . 3 class 1
4 caddc 7630 . . 3 class +
52, 3, 4co 5774 . 2 class (6 + 1)
61, 5wceq 1331 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  8810  7pos  8829  7m1e6  8851  6p1e7  8865  4p3e7  8871  5p2e7  8873  6p2e8  8876  7nn  8893  6lt7  8911  7p7e14  9267  8p7e15  9273  9p7e16  9280  9p8e17  9281  7t7e49  9302  8t7e56  9308  9t7e63  9315
  Copyright terms: Public domain W3C validator