Theorem remulcl 8297

Description: Alias for ax-mulrcl 8268, for naming consistency with remulcli 8330. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 8268	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6075   RRcr 8168   x. cmul 8174

This theorem was proved from axioms:  ax-mulrcl 8268

This theorem is referenced by:  remulcli  8330  remulcld  8346  axmulgt0  8387  msqge0  8934  mulge0  8937  recexaplem2  8970  recexap  8971  ltmul12a  9180  lemul12b  9181  mulgt1  9183  ltdivmul  9196  cju  9281  addltmul  9521  zmulcl  9677  irrmul  10026  rpmulcl  10058  ge0mulcl  10363  iccdil  10379  reexpcl  10971  reexpclzap  10974  expge0  10990  expge1  10991  expubnd  11011  bernneq  11076  faclbnd  11157  faclbnd3  11159  facavg  11162  crre  11600  remim  11603  mulreap  11607  amgm2  11862  fprodrecl  12353  fprodreclf  12359  efcllemp  12403  ege2le3  12416  ef01bndlem  12501  cos01gt0  12508  4sqlem11  13158  dveflem  15750  sinq12gt0  15854  tangtx  15862  coskpi  15872  relogexp  15896  logfac  15918  logcxp  15922  rpabscxpbnd  15965