![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-7 | Unicode version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 8964 |
. 2
![]() ![]() | |
2 | c6 8963 |
. . 3
![]() ![]() | |
3 | c1 7803 |
. . 3
![]() ![]() | |
4 | caddc 7805 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5869 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 7re 8991 7pos 9010 7m1e6 9032 6p1e7 9046 4p3e7 9052 5p2e7 9054 6p2e8 9057 7nn 9074 6lt7 9092 7p7e14 9451 8p7e15 9457 9p7e16 9464 9p8e17 9465 7t7e49 9486 8t7e56 9492 9t7e63 9499 lgsdir2lem3 14098 |
Copyright terms: Public domain | W3C validator |