Theorem mulcld 7980

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 7940	. 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 5877   CCcc 7811   x. cmul 7818

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

This theorem is referenced by:  kcnktkm1cn  8342  rereim  8545  cru  8561  apreim  8562  mulreim  8563  apadd1  8567  apneg  8570  mulext1  8571  mulext  8573  aprcl  8605  aptap  8609  mulap0  8613  receuap  8628  mul0eqap  8629  divrecap  8647  divcanap3  8657  muldivdirap  8666  divdivdivap  8672  divsubdivap  8687  apmul1  8747  apdivmuld  8772  qapne  9641  cnref1o  9652  mul2lt0rlt0  9761  lincmb01cmp  10005  iccf1o  10006  qbtwnrelemcalc  10258  flqpmodeq  10329  modq0  10331  modqdiffl  10337  modqvalp1  10345  modqcyc  10361  modqcyc2  10362  modqadd1  10363  mulqaddmodid  10366  modqmuladdnn0  10370  qnegmod  10371  modqmul1  10379  mulexpzap  10562  expmulzap  10568  binom2  10634  binom3  10640  bernneq  10643  mulsubdivbinom2ap  10693  nn0opthd  10704  bcval5  10745  remullem  10882  cjreim2  10915  cnrecnv  10921  absval  11012  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemnm  11029  absimle  11095  abstri  11115  bdtrilem  11249  mulcn2  11322  reccn2ap  11323  climcvg1nlem  11359  isummulc2  11436  fsummulc2  11458  fsumparts  11480  binomlem  11493  binom1dif  11497  trireciplem  11510  mertenslemi1  11545  mertensabs  11547  ntrivcvgap  11558  fprodmul  11601  efaddlem  11684  sinval  11712  cosval  11713  sinadd  11746  cosadd  11747  tanaddaplem  11748  tanaddap  11749  addsin  11752  sincossq  11758  sin2t  11759  cos12dec  11777  eirraplem  11786  dvdscmulr  11829  dvdsmulcr  11830  dvds2ln  11833  oddm1even  11882  divalglemnn  11925  divalglemnqt  11927  flodddiv4  11941  gcdaddm  11987  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  lcmgcdlem  12079  oddpwdc  12176  phiprmpw  12224  eulerthlema  12232  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pcpremul  12295  pcaddlem  12340  fldivp1  12348  mul4sqlem  12393  oddennn  12395  mulc1cncf  14161  mulcncf  14176  dvmulxxbr  14251  dvimulf  14255  dvexp  14260  dvmptmulx  14267  dvmptcmulcn  14268  sin0pilem1  14287  rpcxpef  14400  rpcncxpcl  14408  cxpap0  14410  rpcxpadd  14411  rpmulcxp  14415  cxpmul  14418  abscxp  14420  rpabscxpbnd  14444  binom4  14482  2sqlem3  14549  qdencn  14860  cvgcmp2nlemabs  14865