Theorem mulcli 8279

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

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125   · cmul 8132

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

This theorem is referenced by:  ixi  8857  2mulicn  9460  numma  9752  nummac  9753  9t11e99  9838  decbin2  9849  irec  11001  binom2i  11010  3dec  11076  rei  11584  imi  11585  3dvdsdec  12551  3dvds2dec  12552  odd2np1  12559  3lcm2e6woprm  12783  6lcm4e12  12784  modxai  13114  karatsuba  13128  sinhalfpilem  15656  ef2pi  15670  ef2kpi  15671  efper  15672  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  sin2pim  15678  cos2pim  15679  sincos4thpi  15705  sincos6thpi  15707  abssinper  15711  cosq34lt1  15715  lgsdir2lem5  15905  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983