![]() |
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 8806 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 4re 8821 |
. . 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 df-4 8805 df-5 8806 |
This theorem is referenced by: 5cn 8824 6re 8825 6pos 8845 3lt5 8920 2lt5 8921 1lt5 8922 5lt6 8923 4lt6 8924 5lt7 8929 4lt7 8930 5lt8 8936 4lt8 8937 5lt9 8944 4lt9 8945 5lt10 9340 4lt10 9341 5recm6rec 9349 ef01bndlem 11499 |
Copyright terms: Public domain | W3C validator |