![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 8re | Unicode version |
Description: The number 8 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
8re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 8986 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 7re 9004 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7958 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7972 |
. 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 7907 ax-addrcl 7910 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 df-2 8980 df-3 8981 df-4 8982 df-5 8983 df-6 8984 df-7 8985 df-8 8986 |
This theorem is referenced by: 8cn 9007 9re 9008 9pos 9025 6lt8 9112 5lt8 9113 4lt8 9114 3lt8 9115 2lt8 9116 1lt8 9117 8lt9 9118 7lt9 9119 8th4div3 9140 8lt10 9517 7lt10 9518 ef01bndlem 11766 cos2bnd 11770 slotstnscsi 12655 slotsdnscsi 12679 2lgsoddprmlem1 14538 2lgsoddprmlem2 14539 2lgsoddprmlem3a 14540 2lgsoddprmlem3b 14541 2lgsoddprmlem3c 14542 2lgsoddprmlem3d 14543 |
Copyright terms: Public domain | W3C validator |