![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3re | Unicode version |
Description: The number 3 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
3re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 8977 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 2re 8987 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7955 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7969 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2250 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1re 7904 ax-addrcl 7907 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 df-2 8976 df-3 8977 |
This theorem is referenced by: 3cn 8992 4re 8994 3ne0 9012 3ap0 9013 4pos 9014 1lt3 9088 3lt4 9089 2lt4 9090 3lt5 9093 3lt6 9098 2lt6 9099 3lt7 9104 2lt7 9105 3lt8 9111 2lt8 9112 3lt9 9119 2lt9 9120 1le3 9128 8th4div3 9136 halfpm6th 9137 3halfnz 9348 3lt10 9518 2lt10 9519 uzuzle23 9569 uz3m2nn 9571 nn01to3 9615 3rp 9657 fz0to4untppr 10121 expnass 10622 sqrt9 11052 ef01bndlem 11759 sin01bnd 11760 cos2bnd 11763 sin01gt0 11764 cos01gt0 11765 egt2lt3 11782 flodddiv4 11933 starvndxnmulrndx 12596 scandxnmulrndx 12608 vscandxnmulrndx 12613 ipndxnmulrndx 12626 tsetndxnmulrndx 12642 plendxnmulrndx 12656 dsndxnmulrndx 12667 slotsdifunifndx 12677 dveflem 14080 sincosq3sgn 14142 sincosq4sgn 14143 cosq23lt0 14147 coseq0q4123 14148 coseq00topi 14149 coseq0negpitopi 14150 tangtx 14152 sincos6thpi 14156 pigt3 14158 pige3 14159 cos02pilt1 14165 lgsdir2lem1 14322 ex-fl 14359 ex-gcd 14365 |
Copyright terms: Public domain | W3C validator |