![]() |
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 8969 |
. 2
![]() ![]() | |
2 | c2 8968 |
. . 3
![]() ![]() | |
3 | c1 7811 |
. . 3
![]() ![]() | |
4 | caddc 7813 |
. . 3
![]() ![]() | |
5 | 2, 3, 4 | co 5874 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3re 8991 3pos 9011 3m1e2 9037 2p2e4 9044 2p1e3 9050 3p3e6 9059 4p3e7 9061 5p3e8 9064 6p3e9 9067 3t3e9 9074 3nn 9079 2lt3 9087 7p3e10 9456 7p6e13 9459 8p3e11 9462 8p5e13 9464 9p3e12 9469 9p4e13 9470 4t3e12 9479 5t3e15 9482 6t3e18 9486 7t3e21 9491 8t3e24 9497 9t3e27 9504 nn01to3 9615 fztpval 10080 fz0to3un2pr 10120 fz0to4untppr 10121 fzo0to42pr 10217 cu2 10615 i3 10618 binom3 10634 fac3 10707 ege2le3 11674 ef4p 11697 cos1bnd 11762 3prm 12122 oddprmge3 12129 dveflem 14080 sincosq3sgn 14142 sincosq4sgn 14143 tangtx 14152 sincos6thpi 14156 binom4 14290 lgsdir2lem3 14324 |
Copyright terms: Public domain | W3C validator |