![]() |
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 8985 | . 2 class 3 | |
2 | c2 8984 | . . 3 class 2 | |
3 | c1 7826 | . . 3 class 1 | |
4 | caddc 7828 | . . 3 class + | |
5 | 2, 3, 4 | co 5888 | . 2 class (2 + 1) |
6 | 1, 5 | wceq 1363 | 1 wff 3 = (2 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 3re 9007 3pos 9027 3m1e2 9053 2p2e4 9060 2p1e3 9066 3p3e6 9075 4p3e7 9077 5p3e8 9080 6p3e9 9083 3t3e9 9090 3nn 9095 2lt3 9103 7p3e10 9472 7p6e13 9475 8p3e11 9478 8p5e13 9480 9p3e12 9485 9p4e13 9486 4t3e12 9495 5t3e15 9498 6t3e18 9502 7t3e21 9507 8t3e24 9513 9t3e27 9520 nn01to3 9631 fztpval 10097 fz0to3un2pr 10137 fz0to4untppr 10138 fzo0to42pr 10234 cu2 10633 i3 10636 binom3 10652 fac3 10726 ege2le3 11693 ef4p 11716 cos1bnd 11781 3prm 12142 oddprmge3 12149 dveflem 14483 sincosq3sgn 14545 sincosq4sgn 14546 tangtx 14555 sincos6thpi 14559 binom4 14693 lgsdir2lem3 14727 |
Copyright terms: Public domain | W3C validator |