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 7965 | . 2 class 3 | |
2 | c2 7964 | . . 3 class 2 | |
3 | c1 6890 | . . 3 class 1 | |
4 | caddc 6892 | . . 3 class + | |
5 | 2, 3, 4 | co 5512 | . 2 class (2 + 1) |
6 | 1, 5 | wceq 1243 | 1 wff 3 = (2 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 3re 7989 3pos 8010 3m1e2 8036 2p2e4 8037 2p1e3 8043 3p3e6 8053 4p3e7 8055 5p3e8 8058 6p3e9 8062 7p3e10 8065 3t3e9 8072 3nn 8078 2lt3 8087 7p6e13 8421 8p3e11 8423 8p5e13 8425 9p3e12 8430 9p4e13 8431 4t3e12 8439 5t3e15 8441 6t3e18 8445 7t3e21 8450 8t3e24 8456 9t3e27 8463 nn01to3 8552 fztpval 8945 fzo0to42pr 9076 cu2 9351 i3 9354 binom3 9366 |
Copyright terms: Public domain | W3C validator |