HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the number 3. |
| Ref | Expression |
|---|---|
| df-3 |
        |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c3 5909 |
. 2
 | |
| 2 | c2 5908 |
. . 3
| |
| 3 | c1 5207 |
. . 3
| |
| 4 | caddc 5209 |
. . 3
| |
| 5 | 2, 3, 4 | co 3948 |
. 2
|
| 6 | 1, 5 | wceq 953 |
1
 |
| Colors of variables: wff set class |
| This definition is referenced by: 3re 5928 3pos 5938 3nn 5947 2p2e4 5948 3p3e6 5955 4p3e7 5957 5p3e8 5960 6p3e9 5964 7p3e10 5967 3t3e9 5971 halfpm6th 5979 cu2 6571 i3 6663 fac3 6875 fsum4 6963 ele3lem 7268 ege2le3lem2 7271 efaddlem22 7301 ef4p 7340 cos1bnd 7416 sin01gt0 7418 cos01gt0 7419 ruclem1 7453 ruclem3 7455 ipval2 8291 sincosq3sgn 8623 sincosq4sgn 8624 sincos6thpi 8628 stm1add3 10084 stadd3 10085 |