Theorem mulcli 7493

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

Syntax hints:   ∈ wcel 1438  (class class class)co 5652  ℂcc 7348   · cmul 7355

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

This theorem is referenced by:  ixi  8060  2mulicn  8638  numma  8920  nummac  8921  9t11e99  9006  decbin2  9017  irec  10054  binom2i  10063  3dec  10123  rei  10333  imi  10334  3dvdsdec  11143  3dvds2dec  11144  odd2np1  11151  3lcm2e6woprm  11346  6lcm4e12  11347