![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-4 | GIF version |
Description: Define the number 4. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-4 | ⊢ 4 = (3 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c4 8961 | . 2 class 4 | |
2 | c3 8960 | . . 3 class 3 | |
3 | c1 7803 | . . 3 class 1 | |
4 | caddc 7805 | . . 3 class + | |
5 | 2, 3, 4 | co 5869 | . 2 class (3 + 1) |
6 | 1, 5 | wceq 1353 | 1 wff 4 = (3 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 4re 8985 4pos 9005 4m1e3 9029 2p2e4 9035 3p1e4 9043 3p2e5 9049 4p4e8 9053 5p4e9 9056 4nn 9071 3lt4 9080 halfpm6th 9128 6p4e10 9444 7p4e11 9448 7p7e14 9451 8p4e12 9454 8p6e14 9456 9p4e13 9461 9p5e14 9462 4t4e16 9471 5t4e20 9474 6t4e24 9478 7t4e28 9483 8t4e32 9489 9t4e36 9496 fz0to4untppr 10110 fzo0to42pr 10206 4bc2eq6 10738 ef4p 11686 ef01bndlem 11748 sincosq4sgn 13917 binom4 14064 lgsdir2lem3 14098 |
Copyright terms: Public domain | W3C validator |