![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-4 | Unicode version |
Description: Define the number 4. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c4 8631 |
. 2
![]() ![]() | |
2 | c3 8630 |
. . 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: 4re 8655 4pos 8675 2p2e4 8699 3p1e4 8707 3p2e5 8713 4p4e8 8717 5p4e9 8720 4nn 8735 3lt4 8744 halfpm6th 8792 6p4e10 9105 7p4e11 9109 7p7e14 9112 8p4e12 9115 8p6e14 9117 9p4e13 9122 9p5e14 9123 4t4e16 9132 5t4e20 9135 6t4e24 9139 7t4e28 9144 8t4e32 9150 9t4e36 9157 fzo0to42pr 9838 4bc2eq6 10361 ef4p 11198 ef01bndlem 11261 |
Copyright terms: Public domain | W3C validator |