Theorem remulcl 8220

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6028   RRcr 8091   x. cmul 8097

This theorem was proved from axioms:  ax-mulrcl 8191

This theorem is referenced by:  remulcli  8253  remulcld  8269  axmulgt0  8310  msqge0  8855  mulge0  8858  recexaplem2  8891  recexap  8892  ltmul12a  9099  lemul12b  9100  mulgt1  9102  ltdivmul  9115  cju  9200  addltmul  9440  zmulcl  9594  irrmul  9942  rpmulcl  9974  ge0mulcl  10278  iccdil  10294  reexpcl  10881  reexpclzap  10884  expge0  10900  expge1  10901  expubnd  10921  bernneq  10985  faclbnd  11066  faclbnd3  11068  facavg  11071  crre  11497  remim  11500  mulreap  11504  amgm2  11758  fprodrecl  12249  fprodreclf  12255  efcllemp  12299  ege2le3  12312  ef01bndlem  12397  cos01gt0  12404  4sqlem11  13054  dveflem  15537  sinq12gt0  15641  tangtx  15649  coskpi  15659  relogexp  15683  logcxp  15708  rpabscxpbnd  15751