Theorem mulcld 7045

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 7006	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1393  (class class class)co 5512  ℂcc 6885   · cmul 6892

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

This theorem is referenced by:  kcnktkm1cn  7378  rereim  7575  cru  7591  apreim  7592  mulreim  7593  apadd1  7597  apneg  7600  mulext1  7601  mulext  7603  mulap0  7633  receuap  7648  divrecap  7665  divcanap3  7673  divdivdivap  7687  divsubdivap  7702  apmul1  7762  qapne  8572  cnref1o  8580  lincmb01cmp  8869  iccf1o  8870  qbtwnrelemcalc  9108  mulexpzap  9269  expmulzap  9275  binom2  9336  binom3  9340  bernneq  9343  remullem  9445  cjreim2  9478  cnrecnv  9484  absval  9573  resqrexlemover  9582  resqrexlemcalc1  9586  resqrexlemnm  9590  absimle  9654  abstri  9674  mulcn2  9807  iisermulc2  9834  climcvg1nlem  9842  qdencn  10097