Theorem remulcl 8055

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176  (class class class)co 5946   RRcr 7926   x. cmul 7932

This theorem was proved from axioms:  ax-mulrcl 8026

This theorem is referenced by:  remulcli  8088  remulcld  8105  axmulgt0  8146  msqge0  8691  mulge0  8694  recexaplem2  8727  recexap  8728  ltmul12a  8935  lemul12b  8936  mulgt1  8938  ltdivmul  8951  cju  9036  addltmul  9276  zmulcl  9428  irrmul  9770  rpmulcl  9802  ge0mulcl  10106  iccdil  10122  reexpcl  10703  reexpclzap  10706  expge0  10722  expge1  10723  expubnd  10743  bernneq  10807  faclbnd  10888  faclbnd3  10890  facavg  10893  crre  11201  remim  11204  mulreap  11208  amgm2  11462  fprodrecl  11952  fprodreclf  11958  efcllemp  12002  ege2le3  12015  ef01bndlem  12100  cos01gt0  12107  4sqlem11  12757  dveflem  15231  sinq12gt0  15335  tangtx  15343  coskpi  15353  relogexp  15377  logcxp  15402  rpabscxpbnd  15445