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 8736 | . 2 | |
2 | c2 8735 | . . 3 | |
3 | c1 7589 | . . 3 | |
4 | caddc 7591 | . . 3 | |
5 | 2, 3, 4 | co 5742 | . 2 |
6 | 1, 5 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 3re 8758 3pos 8778 3m1e2 8804 2p2e4 8805 2p1e3 8811 3p3e6 8820 4p3e7 8822 5p3e8 8825 6p3e9 8828 3t3e9 8835 3nn 8840 2lt3 8848 7p3e10 9214 7p6e13 9217 8p3e11 9220 8p5e13 9222 9p3e12 9227 9p4e13 9228 4t3e12 9237 5t3e15 9240 6t3e18 9244 7t3e21 9249 8t3e24 9255 9t3e27 9262 nn01to3 9365 fztpval 9818 fzo0to42pr 9952 cu2 10346 i3 10349 binom3 10364 fac3 10433 ege2le3 11291 ef4p 11314 cos1bnd 11380 3prm 11721 oddprmge3 11727 dveflem 12766 sincosq3sgn 12820 sincosq4sgn 12821 |
Copyright terms: Public domain | W3C validator |