![]() |
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 8632 |
. 2
![]() ![]() | |
2 | c4 8631 |
. . 3
![]() ![]() | |
3 | c1 7501 |
. . 3
![]() ![]() | |
4 | caddc 7503 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5706 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 5re 8657 5pos 8678 4p1e5 8708 3p2e5 8713 4p2e6 8715 5nn 8736 4lt5 8747 5p5e10 9104 6p5e11 9106 7p5e12 9110 8p5e13 9116 8p7e15 9118 9p5e14 9123 9p6e15 9124 5t5e25 9136 6t5e30 9140 7t5e35 9145 8t5e40 9151 9t5e45 9158 fldiv4p1lem1div2 9919 ef01bndlem 11261 ex-exp 12542 ex-fac 12543 ex-bc 12544 |
Copyright terms: Public domain | W3C validator |