Theorem mulcli 8295

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

Syntax hints:   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

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

This theorem is referenced by:  ixi  8874  2mulicn  9477  numma  9770  nummac  9771  9t11e99  9856  decbin2  9867  irec  11025  binom2i  11034  3dec  11101  rei  11609  imi  11610  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  3lcm2e6woprm  12808  6lcm4e12  12809  modxai  13139  karatsuba  13153  ballotfilemth  13225  sinhalfpilem  15782  ef2pi  15796  ef2kpi  15797  efper  15798  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  sin2pim  15804  cos2pim  15805  sincos4thpi  15831  sincos6thpi  15833  abssinper  15837  cosq34lt1  15841  lgsdir2lem5  16031  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109