Theorem mulcli 8031

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

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

This theorem is referenced by:  ixi  8610  2mulicn  9213  numma  9500  nummac  9501  9t11e99  9586  decbin2  9597  irec  10731  binom2i  10740  3dec  10806  rei  11064  imi  11065  3dvdsdec  12030  3dvds2dec  12031  odd2np1  12038  3lcm2e6woprm  12254  6lcm4e12  12255  modxai  12585  karatsuba  12599  sinhalfpilem  15027  ef2pi  15041  ef2kpi  15042  efper  15043  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  sin2pim  15049  cos2pim  15050  sincos4thpi  15076  sincos6thpi  15078  abssinper  15082  cosq34lt1  15086  lgsdir2lem5  15273  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351