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 8101 | . 2 | |
2 | 4re 8116 | . . 3 | |
3 | 1re 7118 | . . 3 | |
4 | 2, 3 | readdcli 7132 | . 2 |
5 | 1, 4 | eqeltri 2151 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1433 (class class class)co 5532 cr 6980 c1 6982 caddc 6984 c4 8091 c5 8092 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 ax-ext 2063 ax-1re 7070 ax-addrcl 7073 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 df-clel 2077 df-2 8098 df-3 8099 df-4 8100 df-5 8101 |
This theorem is referenced by: 5cn 8119 6re 8120 6pos 8140 3lt5 8208 2lt5 8209 1lt5 8210 5lt6 8211 4lt6 8212 5lt7 8217 4lt7 8218 5lt8 8224 4lt8 8225 5lt9 8232 4lt9 8233 5lt10 8611 4lt10 8612 |
Copyright terms: Public domain | W3C validator |