![]() |
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 8980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 5re 8996 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7955 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7969 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2250 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1re 7904 ax-addrcl 7907 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 df-2 8976 df-3 8977 df-4 8978 df-5 8979 df-6 8980 |
This theorem is referenced by: 6cn 8999 7re 9000 7pos 9019 4lt6 9097 3lt6 9098 2lt6 9099 1lt6 9100 6lt7 9101 5lt7 9102 6lt8 9108 5lt8 9109 6lt9 9116 5lt9 9117 8th4div3 9136 halfpm6th 9137 div4p1lem1div2 9170 6lt10 9515 5lt10 9516 5recm6rec 9525 efi4p 11720 resin4p 11721 recos4p 11722 ef01bndlem 11759 sin01bnd 11760 cos01bnd 11761 slotsdifipndx 12627 slotstnscsi 12644 plendxnvscandx 12658 slotsdnscsi 12668 sincos6thpi 14156 pigt3 14158 |
Copyright terms: Public domain | W3C validator |