Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-3 | Unicode version |
Description: Define the number 3. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c3 8900 | . 2 | |
2 | c2 8899 | . . 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: 3re 8922 3pos 8942 3m1e2 8968 2p2e4 8975 2p1e3 8981 3p3e6 8990 4p3e7 8992 5p3e8 8995 6p3e9 8998 3t3e9 9005 3nn 9010 2lt3 9018 7p3e10 9387 7p6e13 9390 8p3e11 9393 8p5e13 9395 9p3e12 9400 9p4e13 9401 4t3e12 9410 5t3e15 9413 6t3e18 9417 7t3e21 9422 8t3e24 9428 9t3e27 9435 nn01to3 9546 fztpval 10008 fz0to3un2pr 10048 fz0to4untppr 10049 fzo0to42pr 10145 cu2 10543 i3 10546 binom3 10561 fac3 10634 ege2le3 11598 ef4p 11621 cos1bnd 11686 3prm 12039 oddprmge3 12046 dveflem 13234 sincosq3sgn 13296 sincosq4sgn 13297 tangtx 13306 sincos6thpi 13310 binom4 13444 |
Copyright terms: Public domain | W3C validator |