Theorem mulcli 8227

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

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

This theorem is referenced by:  ixi  8805  2mulicn  9408  numma  9698  nummac  9699  9t11e99  9784  decbin2  9795  irec  10947  binom2i  10956  3dec  11022  rei  11522  imi  11523  3dvdsdec  12489  3dvds2dec  12490  odd2np1  12497  3lcm2e6woprm  12721  6lcm4e12  12722  modxai  13052  karatsuba  13066  sinhalfpilem  15585  ef2pi  15599  ef2kpi  15600  efper  15601  sinperlem  15602  sin2kpi  15605  cos2kpi  15606  sin2pim  15607  cos2pim  15608  sincos4thpi  15634  sincos6thpi  15636  abssinper  15640  cosq34lt1  15644  lgsdir2lem5  15834  2lgsoddprmlem3c  15911  2lgsoddprmlem3d  15912