Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 6re | Unicode version |
Description: The number 6 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
6re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 8102 | . 2 | |
2 | 5re 8118 | . . 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 c5 8092 c6 8093 |
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 df-6 8102 |
This theorem is referenced by: 6cn 8121 7re 8122 7pos 8141 4lt6 8212 3lt6 8213 2lt6 8214 1lt6 8215 6lt7 8216 5lt7 8217 6lt8 8223 5lt8 8224 6lt9 8231 5lt9 8232 8th4div3 8250 halfpm6th 8251 div4p1lem1div2 8284 6lt10 8610 5lt10 8611 |
Copyright terms: Public domain | W3C validator |