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

Definition df-7 8981
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 8973 . 2 class 7
2 c6 8972 . . 3 class 6
3 c1 7811 . . 3 class 1
4 caddc 7813 . . 3 class +
52, 3, 4co 5874 . 2 class (6 + 1)
61, 5wceq 1353 1 wff 7 = (6 + 1)
Colors of variables: wff set class
This definition is referenced by:  7re  9000  7pos  9019  7m1e6  9041  6p1e7  9055  4p3e7  9061  5p2e7  9063  6p2e8  9066  7nn  9083  6lt7  9101  7p7e14  9460  8p7e15  9466  9p7e16  9473  9p8e17  9474  7t7e49  9495  8t7e56  9501  9t7e63  9508  lgsdir2lem3  14324
  Copyright terms: Public domain W3C validator