Theorem mulcld 7605

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 7566	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	syl2anc 404	1 |- ( ph -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1445  (class class class)co 5690   CCcc 7445   x. cmul 7452

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

This theorem is referenced by:  kcnktkm1cn  7958  rereim  8160  cru  8176  apreim  8177  mulreim  8178  apadd1  8182  apneg  8185  mulext1  8186  mulext  8188  mulap0  8220  receuap  8235  divrecap  8252  divcanap3  8262  muldivdirap  8271  divdivdivap  8277  divsubdivap  8292  apmul1  8352  apdivmuld  8377  qapne  9223  cnref1o  9232  lincmb01cmp  9569  iccf1o  9570  qbtwnrelemcalc  9816  flqpmodeq  9883  modq0  9885  modqdiffl  9891  modqvalp1  9899  modqcyc  9915  modqcyc2  9916  modqadd1  9917  mulqaddmodid  9920  modqmuladdnn0  9924  qnegmod  9925  modqmul1  9933  mulexpzap  10126  expmulzap  10132  binom2  10196  binom3  10202  bernneq  10205  nn0opthd  10261  bcval5  10302  remullem  10436  cjreim2  10469  cnrecnv  10475  absval  10565  resqrexlemover  10574  resqrexlemcalc1  10578  resqrexlemnm  10582  absimle  10648  abstri  10668  bdtrilem  10801  mulcn2  10871  climcvg1nlem  10907  isummulc2  10984  fsummulc2  11006  fsumparts  11028  binomlem  11041  binom1dif  11045  trireciplem  11058  mertenslemi1  11093  mertensabs  11095  efaddlem  11128  sinval  11157  cosval  11158  sinadd  11191  cosadd  11192  tanaddaplem  11193  tanaddap  11194  addsin  11197  sincossq  11203  sin2t  11204  eirraplem  11228  dvdscmulr  11267  dvdsmulcr  11268  dvds2ln  11271  oddm1even  11317  divalglemnn  11360  divalglemnqt  11362  flodddiv4  11376  gcdaddm  11417  bezoutlemnewy  11427  bezoutlema  11430  bezoutlemb  11431  lcmgcdlem  11501  oddpwdc  11594  phiprmpw  11640  oddennn  11647  mulc1cncf  12357  qdencn  12624