Theorem mulcld 7253

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

Syntax hints:   -> wi 4   e. wcel 1434  (class class class)co 5563   CCcc 7093   x. cmul 7100

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

This theorem is referenced by:  kcnktkm1cn  7606  rereim  7805  cru  7821  apreim  7822  mulreim  7823  apadd1  7827  apneg  7830  mulext1  7831  mulext  7833  mulap0  7863  receuap  7878  divrecap  7895  divcanap3  7905  muldivdirap  7914  divdivdivap  7920  divsubdivap  7935  apmul1  7995  qapne  8857  cnref1o  8866  lincmb01cmp  9153  iccf1o  9154  qbtwnrelemcalc  9394  flqpmodeq  9461  modq0  9463  modqdiffl  9469  modqvalp1  9477  modqcyc  9493  modqcyc2  9494  modqadd1  9495  mulqaddmodid  9498  modqmuladdnn0  9502  qnegmod  9503  modqmul1  9511  mulexpzap  9665  expmulzap  9671  binom2  9734  binom3  9739  bernneq  9742  nn0opthd  9798  ibcval5  9839  remullem  9959  cjreim2  9992  cnrecnv  9998  absval  10088  resqrexlemover  10097  resqrexlemcalc1  10101  resqrexlemnm  10105  absimle  10171  abstri  10191  mulcn2  10352  iisermulc2  10379  climcvg1nlem  10387  dvdscmulr  10432  dvdsmulcr  10433  dvds2ln  10436  oddm1even  10482  divalglemnn  10525  divalglemnqt  10527  flodddiv4  10541  gcdaddm  10582  bezoutlemnewy  10592  bezoutlema  10595  bezoutlemb  10596  lcmgcdlem  10666  oddpwdc  10759  phiprmpw  10805  oddennn  10812  qdencn  11052