![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-5 | Unicode version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 8998 |
. 2
![]() ![]() | |
2 | c4 8997 |
. . 3
![]() ![]() | |
3 | c1 7837 |
. . 3
![]() ![]() | |
4 | caddc 7839 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5892 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 5re 9023 5pos 9044 5m1e4 9066 4p1e5 9080 3p2e5 9085 4p2e6 9087 5nn 9108 4lt5 9119 5p5e10 9479 6p5e11 9481 7p5e12 9485 8p5e13 9491 8p7e15 9493 9p5e14 9498 9p6e15 9499 5t5e25 9511 6t5e30 9515 7t5e35 9520 8t5e40 9526 9t5e45 9533 fldiv4p1lem1div2 10331 ef01bndlem 11791 prm23lt5 12290 lgsdir2lem3 14868 2lgsoddprmlem3c 14894 ex-exp 14916 ex-fac 14917 ex-bc 14918 |
Copyright terms: Public domain | W3C validator |