Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-6 | GIF version |
Description: Define the number 6. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-6 | ⊢ 6 = (5 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c6 8933 | . 2 class 6 | |
2 | c5 8932 | . . 3 class 5 | |
3 | c1 7775 | . . 3 class 1 | |
4 | caddc 7777 | . . 3 class + | |
5 | 2, 3, 4 | co 5853 | . 2 class (5 + 1) |
6 | 1, 5 | wceq 1348 | 1 wff 6 = (5 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 6re 8959 6pos 8979 6m1e5 9001 5p1e6 9015 3p3e6 9020 4p2e6 9021 5p2e7 9024 6nn 9043 5lt6 9057 6p6e12 9416 7p6e13 9420 8p6e14 9426 8p8e16 9428 9p6e15 9433 9p7e16 9434 6t6e36 9450 7t6e42 9455 8t6e48 9461 9t6e54 9468 lgsdir2lem3 13725 |
Copyright terms: Public domain | W3C validator |