Theorem mulcli 8010

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

Syntax hints:   ∈ wcel 2160  (class class class)co 5906  ℂcc 7856   · cmul 7863

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

This theorem is referenced by:  ixi  8588  2mulicn  9190  numma  9477  nummac  9478  9t11e99  9563  decbin2  9574  irec  10684  binom2i  10693  3dec  10759  rei  11017  imi  11018  3dvdsdec  11980  3dvds2dec  11981  odd2np1  11988  3lcm2e6woprm  12198  6lcm4e12  12199  sinhalfpilem  14854  ef2pi  14868  ef2kpi  14869  efper  14870  sinperlem  14871  sin2kpi  14874  cos2kpi  14875  sin2pim  14876  cos2pim  14877  sincos4thpi  14903  sincos6thpi  14905  abssinper  14909  cosq34lt1  14913  lgsdir2lem5  15076  2lgsoddprmlem3c  15121  2lgsoddprmlem3d  15122