Theorem mulcli 8026

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 8001	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 426	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

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

This theorem is referenced by:  ixi  8604  2mulicn  9207  numma  9494  nummac  9495  9t11e99  9580  decbin2  9591  irec  10713  binom2i  10722  3dec  10788  rei  11046  imi  11047  3dvdsdec  12009  3dvds2dec  12010  odd2np1  12017  3lcm2e6woprm  12227  6lcm4e12  12228  sinhalfpilem  14967  ef2pi  14981  ef2kpi  14982  efper  14983  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  sin2pim  14989  cos2pim  14990  sincos4thpi  15016  sincos6thpi  15018  abssinper  15022  cosq34lt1  15026  lgsdir2lem5  15189  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267