Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3re | Unicode version |
Description: The number 3 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
3re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 7974 | . 2 | |
2 | 2re 7985 | . . 3 | |
3 | 1re 7026 | . . 3 | |
4 | 2, 3 | readdcli 7040 | . 2 |
5 | 1, 4 | eqeltri 2110 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1393 (class class class)co 5512 cr 6888 c1 6890 caddc 6892 c2 7964 c3 7965 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 ax-1re 6978 ax-addrcl 6981 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 df-2 7973 df-3 7974 |
This theorem is referenced by: 3cn 7990 4re 7992 3ne0 8011 3ap0 8012 4pos 8013 1lt3 8088 3lt4 8089 2lt4 8090 3lt5 8093 3lt6 8098 2lt6 8099 3lt7 8104 2lt7 8105 3lt8 8111 2lt8 8112 3lt9 8119 2lt9 8120 3lt10 8128 2lt10 8129 1le3 8136 8th4div3 8144 halfpm6th 8145 uzuzle23 8513 uz3m2nn 8515 nn01to3 8552 expnass 9357 sqrt9 9646 ex-fl 9895 |
Copyright terms: Public domain | W3C validator |