Theorem mulcld 7201

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcl 7162	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 403	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1434  (class class class)co 5543  ℂcc 7041   · cmul 7048

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

This theorem is referenced by:  kcnktkm1cn  7554  rereim  7753  cru  7769  apreim  7770  mulreim  7771  apadd1  7775  apneg  7778  mulext1  7779  mulext  7781  mulap0  7811  receuap  7826  divrecap  7843  divcanap3  7853  muldivdirap  7862  divdivdivap  7868  divsubdivap  7883  apmul1  7943  qapne  8805  cnref1o  8814  lincmb01cmp  9101  iccf1o  9102  qbtwnrelemcalc  9342  flqpmodeq  9409  modq0  9411  modqdiffl  9417  modqvalp1  9425  modqcyc  9441  modqcyc2  9442  modqadd1  9443  mulqaddmodid  9446  modqmuladdnn0  9450  qnegmod  9451  modqmul1  9459  mulexpzap  9613  expmulzap  9619  binom2  9682  binom3  9687  bernneq  9690  nn0opthd  9746  ibcval5  9787  remullem  9896  cjreim2  9929  cnrecnv  9935  absval  10025  resqrexlemover  10034  resqrexlemcalc1  10038  resqrexlemnm  10042  absimle  10108  abstri  10128  mulcn2  10289  iisermulc2  10316  climcvg1nlem  10324  dvdscmulr  10369  dvdsmulcr  10370  dvds2ln  10373  oddm1even  10419  divalglemnn  10462  divalglemnqt  10464  flodddiv4  10478  gcdaddm  10519  bezoutlemnewy  10529  bezoutlema  10532  bezoutlemb  10533  lcmgcdlem  10603  oddpwdc  10696  oddennn  10703  qdencn  10943