Theorem mulcli 7764

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

Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℂcc 7611   · cmul 7618

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

This theorem is referenced by:  ixi  8338  2mulicn  8935  numma  9218  nummac  9219  9t11e99  9304  decbin2  9315  irec  10385  binom2i  10394  3dec  10454  rei  10664  imi  10665  3dvdsdec  11551  3dvds2dec  11552  odd2np1  11559  3lcm2e6woprm  11756  6lcm4e12  11757  sinhalfpilem  12861  ef2pi  12875  ef2kpi  12876  efper  12877  sinperlem  12878  sin2kpi  12881  cos2kpi  12882  sin2pim  12883  cos2pim  12884  sincos4thpi  12910  sincos6thpi  12912  abssinper  12916  cosq34lt1  12920