Theorem mulcli 7124

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

Syntax hints:   ∈ wcel 1433  (class class class)co 5532  ℂcc 6979   · cmul 6986

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

This theorem is referenced by:  ixi  7683  2mulicn  8253  numma  8520  nummac  8521  9t11e99  8606  decbin2  8617  irec  9574  binom2i  9583  3dec  9642  rei  9786  imi  9787  3dvdsdec  10264  3dvds2dec  10265  odd2np1  10272  3lcm2e6woprm  10468  6lcm4e12  10469