![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 5re | Unicode version |
Description: The number 5 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
5re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-5 8640 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 4re 8655 |
. . 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 |
This theorem is referenced by: 5cn 8658 6re 8659 6pos 8679 3lt5 8748 2lt5 8749 1lt5 8750 5lt6 8751 4lt6 8752 5lt7 8757 4lt7 8758 5lt8 8764 4lt8 8765 5lt9 8772 4lt9 8773 5lt10 9168 4lt10 9169 ef01bndlem 11261 |
Copyright terms: Public domain | W3C validator |