Theorem remulcl 7936

Description: Alias for ax-mulrcl 7907, for naming consistency with remulcli 7968. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 7907	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5872  ℝcr 7807   · cmul 7813

This theorem was proved from axioms:  ax-mulrcl 7907

This theorem is referenced by:  remulcli  7968  remulcld  7984  axmulgt0  8025  msqge0  8569  mulge0  8572  recexaplem2  8605  recexap  8606  ltmul12a  8813  lemul12b  8814  mulgt1  8816  ltdivmul  8829  cju  8914  addltmul  9151  zmulcl  9302  irrmul  9643  rpmulcl  9674  ge0mulcl  9978  iccdil  9994  reexpcl  10532  reexpclzap  10535  expge0  10551  expge1  10552  expubnd  10572  bernneq  10635  faclbnd  10714  faclbnd3  10716  facavg  10719  crre  10859  remim  10862  mulreap  10866  amgm2  11120  fprodrecl  11609  fprodreclf  11615  efcllemp  11659  ege2le3  11672  ef01bndlem  11757  cos01gt0  11763  dveflem  14058  sinq12gt0  14122  tangtx  14130  coskpi  14140  relogexp  14164  logcxp  14189  rpabscxpbnd  14230