Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-3 | GIF version |
Description: Define the number 3. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-3 | ⊢ 3 = (2 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c3 8772 | . 2 class 3 | |
2 | c2 8771 | . . 3 class 2 | |
3 | c1 7621 | . . 3 class 1 | |
4 | caddc 7623 | . . 3 class + | |
5 | 2, 3, 4 | co 5774 | . 2 class (2 + 1) |
6 | 1, 5 | wceq 1331 | 1 wff 3 = (2 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 3re 8794 3pos 8814 3m1e2 8840 2p2e4 8847 2p1e3 8853 3p3e6 8862 4p3e7 8864 5p3e8 8867 6p3e9 8870 3t3e9 8877 3nn 8882 2lt3 8890 7p3e10 9256 7p6e13 9259 8p3e11 9262 8p5e13 9264 9p3e12 9269 9p4e13 9270 4t3e12 9279 5t3e15 9282 6t3e18 9286 7t3e21 9291 8t3e24 9297 9t3e27 9304 nn01to3 9409 fztpval 9863 fzo0to42pr 9997 cu2 10391 i3 10394 binom3 10409 fac3 10478 ege2le3 11377 ef4p 11400 cos1bnd 11466 3prm 11809 oddprmge3 11815 dveflem 12855 sincosq3sgn 12909 sincosq4sgn 12910 tangtx 12919 sincos6thpi 12923 |
Copyright terms: Public domain | W3C validator |