Theorem remulcl 7468

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438  (class class class)co 5652   RRcr 7347   x. cmul 7353

This theorem was proved from axioms:  ax-mulrcl 7442

This theorem is referenced by:  remulcli  7500  remulcld  7516  axmulgt0  7556  msqge0  8091  mulge0  8094  recexaplem2  8119  recexap  8120  ltmul12a  8319  lemul12b  8320  mulgt1  8322  ltdivmul  8335  cju  8419  addltmul  8650  zmulcl  8801  irrmul  9130  rpmulcl  9156  ge0mulcl  9398  iccdil  9413  reexpcl  9968  reexpclzap  9971  expge0  9987  expge1  9988  expubnd  10008  bernneq  10070  faclbnd  10145  faclbnd3  10147  facavg  10150  crre  10287  remim  10290  mulreap  10294  amgm2  10547  efcllemp  10944  ege2le3  10957  ef01bndlem  11043  cos01gt0  11049