Theorem mulcli 8024

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

Syntax hints:   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

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

This theorem is referenced by:  ixi  8602  2mulicn  9204  numma  9491  nummac  9492  9t11e99  9577  decbin2  9588  irec  10710  binom2i  10719  3dec  10785  rei  11043  imi  11044  3dvdsdec  12006  3dvds2dec  12007  odd2np1  12014  3lcm2e6woprm  12224  6lcm4e12  12225  sinhalfpilem  14926  ef2pi  14940  ef2kpi  14941  efper  14942  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  sin2pim  14948  cos2pim  14949  sincos4thpi  14975  sincos6thpi  14977  abssinper  14981  cosq34lt1  14985  lgsdir2lem5  15148  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198