![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-6 | Unicode version |
Description: Define the number 6. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c6 8977 |
. 2
![]() ![]() | |
2 | c5 8976 |
. . 3
![]() ![]() | |
3 | c1 7815 |
. . 3
![]() ![]() | |
4 | caddc 7817 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5878 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 6re 9003 6pos 9023 6m1e5 9045 5p1e6 9059 3p3e6 9064 4p2e6 9065 5p2e7 9068 6nn 9087 5lt6 9101 6p6e12 9460 7p6e13 9464 8p6e14 9470 8p8e16 9472 9p6e15 9477 9p7e16 9478 6t6e36 9494 7t6e42 9499 8t6e48 9505 9t6e54 9512 lgsdir2lem3 14619 2lgsoddprmlem3d 14646 |
Copyright terms: Public domain | W3C validator |