![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > remulcl | Unicode version |
Description: Alias for ax-mulrcl 7743, for naming consistency with remulcli 7804. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
remulcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulrcl 7743 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulrcl 7743 |
This theorem is referenced by: remulcli 7804 remulcld 7820 axmulgt0 7860 msqge0 8402 mulge0 8405 recexaplem2 8437 recexap 8438 ltmul12a 8642 lemul12b 8643 mulgt1 8645 ltdivmul 8658 cju 8743 addltmul 8980 zmulcl 9131 irrmul 9466 rpmulcl 9495 ge0mulcl 9795 iccdil 9811 reexpcl 10341 reexpclzap 10344 expge0 10360 expge1 10361 expubnd 10381 bernneq 10443 faclbnd 10519 faclbnd3 10521 facavg 10524 crre 10661 remim 10664 mulreap 10668 amgm2 10922 efcllemp 11401 ege2le3 11414 ef01bndlem 11499 cos01gt0 11505 dveflem 12895 sinq12gt0 12959 tangtx 12967 coskpi 12977 relogexp 13001 logcxp 13026 rpabscxpbnd 13067 |
Copyright terms: Public domain | W3C validator |