Theorem mulcli 8162

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008   · cmul 8015

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

This theorem is referenced by:  ixi  8741  2mulicn  9344  numma  9632  nummac  9633  9t11e99  9718  decbin2  9729  irec  10873  binom2i  10882  3dec  10948  rei  11425  imi  11426  3dvdsdec  12391  3dvds2dec  12392  odd2np1  12399  3lcm2e6woprm  12623  6lcm4e12  12624  modxai  12954  karatsuba  12968  sinhalfpilem  15480  ef2pi  15494  ef2kpi  15495  efper  15496  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  sin2pim  15502  cos2pim  15503  sincos4thpi  15529  sincos6thpi  15531  abssinper  15535  cosq34lt1  15539  lgsdir2lem5  15726  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804