Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > remulcl | Unicode version |
Description: Alias for ax-mulrcl 7687, for naming consistency with remulcli 7748. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
remulcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulrcl 7687 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 (class class class)co 5742 cr 7587 cmul 7593 |
This theorem was proved from axioms: ax-mulrcl 7687 |
This theorem is referenced by: remulcli 7748 remulcld 7764 axmulgt0 7804 msqge0 8346 mulge0 8349 recexaplem2 8381 recexap 8382 ltmul12a 8586 lemul12b 8587 mulgt1 8589 ltdivmul 8602 cju 8687 addltmul 8924 zmulcl 9075 irrmul 9407 rpmulcl 9434 ge0mulcl 9733 iccdil 9749 reexpcl 10278 reexpclzap 10281 expge0 10297 expge1 10298 expubnd 10318 bernneq 10380 faclbnd 10455 faclbnd3 10457 facavg 10460 crre 10597 remim 10600 mulreap 10604 amgm2 10858 efcllemp 11291 ege2le3 11304 ef01bndlem 11390 cos01gt0 11396 dveflem 12782 sinq12gt0 12838 tangtx 12846 coskpi 12856 |
Copyright terms: Public domain | W3C validator |