Theorem mulcli 7965

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

Syntax hints:   ∈ wcel 2148  (class class class)co 5878  ℂcc 7812   · cmul 7819

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

This theorem is referenced by:  ixi  8543  2mulicn  9144  numma  9430  nummac  9431  9t11e99  9516  decbin2  9527  irec  10623  binom2i  10632  3dec  10697  rei  10911  imi  10912  3dvdsdec  11873  3dvds2dec  11874  odd2np1  11881  3lcm2e6woprm  12089  6lcm4e12  12090  sinhalfpilem  14373  ef2pi  14387  ef2kpi  14388  efper  14389  sinperlem  14390  sin2kpi  14393  cos2kpi  14394  sin2pim  14395  cos2pim  14396  sincos4thpi  14422  sincos6thpi  14424  abssinper  14428  cosq34lt1  14432  lgsdir2lem5  14594  2lgsoddprmlem3c  14618  2lgsoddprmlem3d  14619