![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-5 | GIF version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 | ⊢ 5 = (4 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 8159 | . 2 class 5 | |
2 | c4 8158 | . . 3 class 4 | |
3 | c1 7044 | . . 3 class 1 | |
4 | caddc 7046 | . . 3 class + | |
5 | 2, 3, 4 | co 5543 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1285 | 1 wff 5 = (4 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 5re 8185 5pos 8206 4p1e5 8235 3p2e5 8240 4p2e6 8242 5nn 8263 4lt5 8274 5p5e10 8628 6p5e11 8630 7p5e12 8634 8p5e13 8640 8p7e15 8642 9p5e14 8647 9p6e15 8648 5t5e25 8660 6t5e30 8664 7t5e35 8669 8t5e40 8675 9t5e45 8682 fldiv4p1lem1div2 9387 ex-fac 10716 ex-bc 10717 |
Copyright terms: Public domain | W3C validator |