Theorem mulcli 8048

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

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   · cmul 7901

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

This theorem is referenced by:  ixi  8627  2mulicn  9230  numma  9517  nummac  9518  9t11e99  9603  decbin2  9614  irec  10748  binom2i  10757  3dec  10823  rei  11081  imi  11082  3dvdsdec  12047  3dvds2dec  12048  odd2np1  12055  3lcm2e6woprm  12279  6lcm4e12  12280  modxai  12610  karatsuba  12624  sinhalfpilem  15111  ef2pi  15125  ef2kpi  15126  efper  15127  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  sin2pim  15133  cos2pim  15134  sincos4thpi  15160  sincos6thpi  15162  abssinper  15166  cosq34lt1  15170  lgsdir2lem5  15357  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435