Theorem remulcl 7942

Description: Alias for ax-mulrcl 7913, for naming consistency with remulcli 7974. (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 7913	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148  (class class class)co 5878   RRcr 7813   x. cmul 7819

This theorem was proved from axioms:  ax-mulrcl 7913

This theorem is referenced by:  remulcli  7974  remulcld  7991  axmulgt0  8032  msqge0  8576  mulge0  8579  recexaplem2  8612  recexap  8613  ltmul12a  8820  lemul12b  8821  mulgt1  8823  ltdivmul  8836  cju  8921  addltmul  9158  zmulcl  9309  irrmul  9650  rpmulcl  9681  ge0mulcl  9985  iccdil  10001  reexpcl  10540  reexpclzap  10543  expge0  10559  expge1  10560  expubnd  10580  bernneq  10644  faclbnd  10724  faclbnd3  10726  facavg  10729  crre  10869  remim  10872  mulreap  10876  amgm2  11130  fprodrecl  11619  fprodreclf  11625  efcllemp  11669  ege2le3  11682  ef01bndlem  11767  cos01gt0  11773  dveflem  14348  sinq12gt0  14412  tangtx  14420  coskpi  14430  relogexp  14454  logcxp  14479  rpabscxpbnd  14520