![]() |
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 9017 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 5re 9033 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7991 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 8005 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2262 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 ax-1re 7940 ax-addrcl 7943 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 df-2 9013 df-3 9014 df-4 9015 df-5 9016 df-6 9017 |
This theorem is referenced by: 6cn 9036 7re 9037 7pos 9056 4lt6 9134 3lt6 9135 2lt6 9136 1lt6 9137 6lt7 9138 5lt7 9139 6lt8 9145 5lt8 9146 6lt9 9153 5lt9 9154 8th4div3 9173 halfpm6th 9174 div4p1lem1div2 9207 6lt10 9552 5lt10 9553 5recm6rec 9562 efi4p 11766 resin4p 11767 recos4p 11768 ef01bndlem 11805 sin01bnd 11806 cos01bnd 11807 slotsdifipndx 12697 slotstnscsi 12717 plendxnvscandx 12731 slotsdnscsi 12741 sincos6thpi 14748 pigt3 14750 |
Copyright terms: Public domain | W3C validator |