Theorem remulcl 8002

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164  (class class class)co 5919   RRcr 7873   x. cmul 7879

This theorem was proved from axioms:  ax-mulrcl 7973

This theorem is referenced by:  remulcli  8035  remulcld  8052  axmulgt0  8093  msqge0  8637  mulge0  8640  recexaplem2  8673  recexap  8674  ltmul12a  8881  lemul12b  8882  mulgt1  8884  ltdivmul  8897  cju  8982  addltmul  9222  zmulcl  9373  irrmul  9715  rpmulcl  9747  ge0mulcl  10051  iccdil  10067  reexpcl  10630  reexpclzap  10633  expge0  10649  expge1  10650  expubnd  10670  bernneq  10734  faclbnd  10815  faclbnd3  10817  facavg  10820  crre  11004  remim  11007  mulreap  11011  amgm2  11265  fprodrecl  11754  fprodreclf  11760  efcllemp  11804  ege2le3  11817  ef01bndlem  11902  cos01gt0  11909  4sqlem11  12542  dveflem  14905  sinq12gt0  15006  tangtx  15014  coskpi  15024  relogexp  15048  logcxp  15073  rpabscxpbnd  15114