Theorem mulcli 8321

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcli	⊢ (𝐴 · 𝐵) ∈ ℂ

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcl 8296	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 430	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   · cmul 8174

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

This theorem is referenced by:  ixi  8901  2mulicn  9506  numma  9799  nummac  9800  9t11e99  9885  decbin2  9896  irec  11054  binom2i  11063  3dec  11130  rei  11643  imi  11644  3dvdsdec  12610  3dvds2dec  12611  odd2np1  12618  3lcm2e6woprm  12842  6lcm4e12  12843  modxai  13173  karatsuba  13187  ballotfilemth  13259  sinhalfpilem  15815  ef2pi  15829  ef2kpi  15830  efper  15831  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  sin2pim  15837  cos2pim  15838  sincos4thpi  15864  sincos6thpi  15866  abssinper  15870  cosq34lt1  15874  lgsdir2lem5  16065  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143