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 7968 | . 2 | |
2 | c5 7967 | . . 3 | |
3 | c1 6890 | . . 3 | |
4 | caddc 6892 | . . 3 | |
5 | 2, 3, 4 | co 5512 | . 2 |
6 | 1, 5 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 6re 7996 6pos 8017 5p1e6 8047 3p3e6 8053 4p2e6 8054 5p2e7 8057 6nn 8081 5lt6 8096 6p6e12 8418 7p6e13 8421 8p6e14 8426 8p8e16 8428 9p6e15 8433 9p7e16 8434 6t6e36 8448 7t6e42 8453 8t6e48 8459 9t6e54 8466 |
Copyright terms: Public domain | W3C validator |