![]() |
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 8804 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 2re 8814 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7789 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7803 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2213 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 ax-1re 7738 ax-addrcl 7741 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 df-2 8803 df-3 8804 |
This theorem is referenced by: 3cn 8819 4re 8821 3ne0 8839 3ap0 8840 4pos 8841 1lt3 8915 3lt4 8916 2lt4 8917 3lt5 8920 3lt6 8925 2lt6 8926 3lt7 8931 2lt7 8932 3lt8 8938 2lt8 8939 3lt9 8946 2lt9 8947 1le3 8955 8th4div3 8963 halfpm6th 8964 3halfnz 9172 3lt10 9342 2lt10 9343 uzuzle23 9393 uz3m2nn 9395 nn01to3 9436 3rp 9476 expnass 10429 sqrt9 10852 ef01bndlem 11499 sin01bnd 11500 cos2bnd 11503 sin01gt0 11504 cos01gt0 11505 egt2lt3 11522 flodddiv4 11667 dveflem 12895 sincosq3sgn 12957 sincosq4sgn 12958 cosq23lt0 12962 coseq0q4123 12963 coseq00topi 12964 coseq0negpitopi 12965 tangtx 12967 sincos6thpi 12971 pigt3 12973 pige3 12974 cos02pilt1 12980 ex-fl 13108 ex-gcd 13114 |
Copyright terms: Public domain | W3C validator |