Theorem mulcli 7925

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

Syntax hints:   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   · cmul 7779

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

This theorem is referenced by:  ixi  8502  2mulicn  9100  numma  9386  nummac  9387  9t11e99  9472  decbin2  9483  irec  10575  binom2i  10584  3dec  10648  rei  10863  imi  10864  3dvdsdec  11824  3dvds2dec  11825  odd2np1  11832  3lcm2e6woprm  12040  6lcm4e12  12041  sinhalfpilem  13506  ef2pi  13520  ef2kpi  13521  efper  13522  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  sincos4thpi  13555  sincos6thpi  13557  abssinper  13561  cosq34lt1  13565  lgsdir2lem5  13727