![]() |
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 8475 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 5re 8491 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7477 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7491 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2160 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 ax-ext 2070 ax-1re 7429 ax-addrcl 7432 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 df-clel 2084 df-2 8471 df-3 8472 df-4 8473 df-5 8474 df-6 8475 |
This theorem is referenced by: 6cn 8494 7re 8495 7pos 8514 4lt6 8586 3lt6 8587 2lt6 8588 1lt6 8589 6lt7 8590 5lt7 8591 6lt8 8597 5lt8 8598 6lt9 8605 5lt9 8606 8th4div3 8625 halfpm6th 8626 div4p1lem1div2 8659 6lt10 9000 5lt10 9001 efi4p 10995 resin4p 10996 recos4p 10997 ef01bndlem 11034 sin01bnd 11035 cos01bnd 11036 |
Copyright terms: Public domain | W3C validator |