Theorem mulcli 8077

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

Syntax hints:   ∈ wcel 2176  (class class class)co 5944  ℂcc 7923   · cmul 7930

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

This theorem is referenced by:  ixi  8656  2mulicn  9259  numma  9547  nummac  9548  9t11e99  9633  decbin2  9644  irec  10784  binom2i  10793  3dec  10859  rei  11210  imi  11211  3dvdsdec  12176  3dvds2dec  12177  odd2np1  12184  3lcm2e6woprm  12408  6lcm4e12  12409  modxai  12739  karatsuba  12753  sinhalfpilem  15263  ef2pi  15277  ef2kpi  15278  efper  15279  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  sin2pim  15285  cos2pim  15286  sincos4thpi  15312  sincos6thpi  15314  abssinper  15318  cosq34lt1  15322  lgsdir2lem5  15509  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587