![]() |
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 8643 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 7re 8661 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7637 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7651 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2172 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 ax-ext 2082 ax-1re 7589 ax-addrcl 7592 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 df-clel 2096 df-2 8637 df-3 8638 df-4 8639 df-5 8640 df-6 8641 df-7 8642 df-8 8643 |
This theorem is referenced by: 8cn 8664 9re 8665 9pos 8682 6lt8 8763 5lt8 8764 4lt8 8765 3lt8 8766 2lt8 8767 1lt8 8768 8lt9 8769 7lt9 8770 8th4div3 8791 8lt10 9165 7lt10 9166 ef01bndlem 11261 cos2bnd 11265 |
Copyright terms: Public domain | W3C validator |