Theorem mulcld 7978

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
mulcld	|- ( ph -> ( A x. B ) e. CC )

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		mulcl 7938	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 2148  (class class class)co 5875   CCcc 7809   x. cmul 7816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 7909

This theorem is referenced by:  kcnktkm1cn  8340  rereim  8543  cru  8559  apreim  8560  mulreim  8561  apadd1  8565  apneg  8568  mulext1  8569  mulext  8571  aprcl  8603  aptap  8607  mulap0  8611  receuap  8626  mul0eqap  8627  divrecap  8645  divcanap3  8655  muldivdirap  8664  divdivdivap  8670  divsubdivap  8685  apmul1  8745  apdivmuld  8770  qapne  9639  cnref1o  9650  mul2lt0rlt0  9759  lincmb01cmp  10003  iccf1o  10004  qbtwnrelemcalc  10256  flqpmodeq  10327  modq0  10329  modqdiffl  10335  modqvalp1  10343  modqcyc  10359  modqcyc2  10360  modqadd1  10361  mulqaddmodid  10364  modqmuladdnn0  10368  qnegmod  10369  modqmul1  10377  mulexpzap  10560  expmulzap  10566  binom2  10632  binom3  10638  bernneq  10641  mulsubdivbinom2ap  10691  nn0opthd  10702  bcval5  10743  remullem  10880  cjreim2  10913  cnrecnv  10919  absval  11010  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemnm  11027  absimle  11093  abstri  11113  bdtrilem  11247  mulcn2  11320  reccn2ap  11321  climcvg1nlem  11357  isummulc2  11434  fsummulc2  11456  fsumparts  11478  binomlem  11491  binom1dif  11495  trireciplem  11508  mertenslemi1  11543  mertensabs  11545  ntrivcvgap  11556  fprodmul  11599  efaddlem  11682  sinval  11710  cosval  11711  sinadd  11744  cosadd  11745  tanaddaplem  11746  tanaddap  11747  addsin  11750  sincossq  11756  sin2t  11757  cos12dec  11775  eirraplem  11784  dvdscmulr  11827  dvdsmulcr  11828  dvds2ln  11831  oddm1even  11880  divalglemnn  11923  divalglemnqt  11925  flodddiv4  11939  gcdaddm  11985  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  lcmgcdlem  12077  oddpwdc  12174  phiprmpw  12222  eulerthlema  12230  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pcpremul  12293  pcaddlem  12338  fldivp1  12346  mul4sqlem  12391  oddennn  12393  mulc1cncf  14079  mulcncf  14094  dvmulxxbr  14169  dvimulf  14173  dvexp  14178  dvmptmulx  14185  dvmptcmulcn  14186  sin0pilem1  14205  rpcxpef  14318  rpcncxpcl  14326  cxpap0  14328  rpcxpadd  14329  rpmulcxp  14333  cxpmul  14336  abscxp  14338  rpabscxpbnd  14362  binom4  14400  2sqlem3  14467  qdencn  14778  cvgcmp2nlemabs  14783