Theorem mulcli 8112

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

Syntax hints:   ∈ wcel 2178  (class class class)co 5967  ℂcc 7958   · cmul 7965

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

This theorem is referenced by:  ixi  8691  2mulicn  9294  numma  9582  nummac  9583  9t11e99  9668  decbin2  9679  irec  10821  binom2i  10830  3dec  10896  rei  11325  imi  11326  3dvdsdec  12291  3dvds2dec  12292  odd2np1  12299  3lcm2e6woprm  12523  6lcm4e12  12524  modxai  12854  karatsuba  12868  sinhalfpilem  15378  ef2pi  15392  ef2kpi  15393  efper  15394  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  sin2pim  15400  cos2pim  15401  sincos4thpi  15427  sincos6thpi  15429  abssinper  15433  cosq34lt1  15437  lgsdir2lem5  15624  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702