Theorem mulcli 7904

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

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751   · cmul 7758

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

This theorem is referenced by:  ixi  8481  2mulicn  9079  numma  9365  nummac  9366  9t11e99  9451  decbin2  9462  irec  10554  binom2i  10563  3dec  10627  rei  10841  imi  10842  3dvdsdec  11802  3dvds2dec  11803  odd2np1  11810  3lcm2e6woprm  12018  6lcm4e12  12019  sinhalfpilem  13352  ef2pi  13366  ef2kpi  13367  efper  13368  sinperlem  13369  sin2kpi  13372  cos2kpi  13373  sin2pim  13374  cos2pim  13375  sincos4thpi  13401  sincos6thpi  13403  abssinper  13407  cosq34lt1  13411  lgsdir2lem5  13573