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 8901 | . 2 | |
2 | c3 8900 | . . 3 | |
3 | c1 7745 | . . 3 | |
4 | caddc 7747 | . . 3 | |
5 | 2, 3, 4 | co 5836 | . 2 |
6 | 1, 5 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 4re 8925 4pos 8945 4m1e3 8969 2p2e4 8975 3p1e4 8983 3p2e5 8989 4p4e8 8993 5p4e9 8996 4nn 9011 3lt4 9020 halfpm6th 9068 6p4e10 9384 7p4e11 9388 7p7e14 9391 8p4e12 9394 8p6e14 9396 9p4e13 9401 9p5e14 9402 4t4e16 9411 5t4e20 9414 6t4e24 9418 7t4e28 9423 8t4e32 9429 9t4e36 9436 fz0to4untppr 10049 fzo0to42pr 10145 4bc2eq6 10676 ef4p 11621 ef01bndlem 11683 sincosq4sgn 13291 binom4 13438 |
Copyright terms: Public domain | W3C validator |