Theorem remulcl 7009

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

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393  (class class class)co 5512   RRcr 6888   x. cmul 6894

This theorem was proved from axioms:  ax-mulrcl 6983

This theorem is referenced by:  remulcli  7041  remulcld  7056  axmulgt0  7091  msqge0  7607  mulge0  7610  recexaplem2  7633  recexap  7634  ltmul12a  7826  lemul12b  7827  mulgt1  7829  ltdivmul  7842  cju  7913  addltmul  8161  zmulcl  8297  irrmul  8581  rpmulcl  8607  ge0mulcl  8851  iccdil  8866  reexpcl  9272  reexpclzap  9275  expge0  9291  expge1  9292  expubnd  9311  bernneq  9369  crre  9457  remim  9460  mulreap  9464  amgm2  9714