Theorem mulcld 7810

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

Syntax hints:   -> wi 4   e. wcel 1481  (class class class)co 5782   CCcc 7642   x. cmul 7649

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

This theorem is referenced by:  kcnktkm1cn  8169  rereim  8372  cru  8388  apreim  8389  mulreim  8390  apadd1  8394  apneg  8397  mulext1  8398  mulext  8400  aprcl  8432  mulap0  8439  receuap  8454  mul0eqap  8455  divrecap  8472  divcanap3  8482  muldivdirap  8491  divdivdivap  8497  divsubdivap  8512  apmul1  8572  apdivmuld  8597  qapne  9458  cnref1o  9469  mul2lt0rlt0  9576  lincmb01cmp  9816  iccf1o  9817  qbtwnrelemcalc  10064  flqpmodeq  10131  modq0  10133  modqdiffl  10139  modqvalp1  10147  modqcyc  10163  modqcyc2  10164  modqadd1  10165  mulqaddmodid  10168  modqmuladdnn0  10172  qnegmod  10173  modqmul1  10181  mulexpzap  10364  expmulzap  10370  binom2  10434  binom3  10440  bernneq  10443  nn0opthd  10500  bcval5  10541  remullem  10675  cjreim2  10708  cnrecnv  10714  absval  10805  resqrexlemover  10814  resqrexlemcalc1  10818  resqrexlemnm  10822  absimle  10888  abstri  10908  bdtrilem  11042  mulcn2  11113  reccn2ap  11114  climcvg1nlem  11150  isummulc2  11227  fsummulc2  11249  fsumparts  11271  binomlem  11284  binom1dif  11288  trireciplem  11301  mertenslemi1  11336  mertensabs  11338  ntrivcvgap  11349  efaddlem  11417  sinval  11445  cosval  11446  sinadd  11479  cosadd  11480  tanaddaplem  11481  tanaddap  11482  addsin  11485  sincossq  11491  sin2t  11492  cos12dec  11510  eirraplem  11519  dvdscmulr  11558  dvdsmulcr  11559  dvds2ln  11562  oddm1even  11608  divalglemnn  11651  divalglemnqt  11653  flodddiv4  11667  gcdaddm  11708  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  lcmgcdlem  11794  oddpwdc  11888  phiprmpw  11934  oddennn  11941  mulc1cncf  12784  mulcncf  12799  dvmulxxbr  12874  dvimulf  12878  dvexp  12883  dvmptmulx  12890  dvmptcmulcn  12891  sin0pilem1  12910  rpcxpef  13023  rpcncxpcl  13031  cxpap0  13033  rpcxpadd  13034  rpmulcxp  13038  cxpmul  13041  abscxp  13043  rpabscxpbnd  13067  qdencn  13397  cvgcmp2nlemabs  13402