Theorem mulcli 8050

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

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

This theorem is referenced by:  ixi  8629  2mulicn  9232  numma  9519  nummac  9520  9t11e99  9605  decbin2  9616  irec  10750  binom2i  10759  3dec  10825  rei  11083  imi  11084  3dvdsdec  12049  3dvds2dec  12050  odd2np1  12057  3lcm2e6woprm  12281  6lcm4e12  12282  modxai  12612  karatsuba  12626  sinhalfpilem  15113  ef2pi  15127  ef2kpi  15128  efper  15129  sinperlem  15130  sin2kpi  15133  cos2kpi  15134  sin2pim  15135  cos2pim  15136  sincos4thpi  15162  sincos6thpi  15164  abssinper  15168  cosq34lt1  15172  lgsdir2lem5  15359  2lgsoddprmlem3c  15436  2lgsoddprmlem3d  15437