Theorem mulcld 7075

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

Syntax hints:   -> wi 4   e. wcel 1407  (class class class)co 5537   CCcc 6915   x. cmul 6922

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

This theorem is referenced by:  kcnktkm1cn  7422  rereim  7621  cru  7637  apreim  7638  mulreim  7639  apadd1  7643  apneg  7646  mulext1  7647  mulext  7649  mulap0  7679  receuap  7694  divrecap  7711  divcanap3  7719  muldivdirap  7728  divdivdivap  7734  divsubdivap  7749  apmul1  7809  qapne  8641  cnref1o  8650  lincmb01cmp  8942  iccf1o  8943  qbtwnrelemcalc  9182  flqpmodeq  9242  modq0  9244  modqdiffl  9250  modqvalp1  9258  modqcyc  9274  modqcyc2  9275  modqadd1  9276  mulqaddmodid  9279  modqmuladdnn0  9283  qnegmod  9284  modqmul1  9292  mulexpzap  9425  expmulzap  9431  binom2  9493  binom3  9498  bernneq  9501  nn0opthd  9554  ibcval5  9595  remullem  9663  cjreim2  9696  cnrecnv  9702  absval  9791  resqrexlemover  9800  resqrexlemcalc1  9804  resqrexlemnm  9808  absimle  9874  abstri  9894  mulcn2  10027  iisermulc2  10054  climcvg1nlem  10062  dvdscmulr  10099  dvdsmulcr  10100  dvds2ln  10103  oddm1even  10149  oddpwdc  10205  qdencn  10454