Theorem remulcl 7748

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480  (class class class)co 5774   RRcr 7619   x. cmul 7625

This theorem was proved from axioms:  ax-mulrcl 7719

This theorem is referenced by:  remulcli  7780  remulcld  7796  axmulgt0  7836  msqge0  8378  mulge0  8381  recexaplem2  8413  recexap  8414  ltmul12a  8618  lemul12b  8619  mulgt1  8621  ltdivmul  8634  cju  8719  addltmul  8956  zmulcl  9107  irrmul  9439  rpmulcl  9466  ge0mulcl  9765  iccdil  9781  reexpcl  10310  reexpclzap  10313  expge0  10329  expge1  10330  expubnd  10350  bernneq  10412  faclbnd  10487  faclbnd3  10489  facavg  10492  crre  10629  remim  10632  mulreap  10636  amgm2  10890  efcllemp  11364  ege2le3  11377  ef01bndlem  11463  cos01gt0  11469  dveflem  12855  sinq12gt0  12911  tangtx  12919  coskpi  12929