![]() |
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 9002 |
. 2
![]() ![]() | |
2 | c3 9001 |
. . 3
![]() ![]() | |
3 | c1 7842 |
. . 3
![]() ![]() | |
4 | caddc 7844 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5896 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 4re 9026 4pos 9046 4m1e3 9070 2p2e4 9076 3p1e4 9084 3p2e5 9090 4p4e8 9094 5p4e9 9097 4nn 9112 3lt4 9121 halfpm6th 9169 6p4e10 9485 7p4e11 9489 7p7e14 9492 8p4e12 9495 8p6e14 9497 9p4e13 9502 9p5e14 9503 4t4e16 9512 5t4e20 9515 6t4e24 9519 7t4e28 9524 8t4e32 9530 9t4e36 9537 fz0to4untppr 10154 fzo0to42pr 10250 4bc2eq6 10786 ef4p 11734 ef01bndlem 11796 sincosq4sgn 14710 binom4 14857 lgsdir2lem3 14892 |
Copyright terms: Public domain | W3C validator |