Theorem mulcli 7883

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

Syntax hints:   ∈ wcel 2128  (class class class)co 5824  ℂcc 7730   · cmul 7737

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

This theorem is referenced by:  ixi  8458  2mulicn  9055  numma  9338  nummac  9339  9t11e99  9424  decbin2  9435  irec  10518  binom2i  10527  3dec  10588  rei  10799  imi  10800  3dvdsdec  11756  3dvds2dec  11757  odd2np1  11764  3lcm2e6woprm  11963  6lcm4e12  11964  sinhalfpilem  13123  ef2pi  13137  ef2kpi  13138  efper  13139  sinperlem  13140  sin2kpi  13143  cos2kpi  13144  sin2pim  13145  cos2pim  13146  sincos4thpi  13172  sincos6thpi  13174  abssinper  13178  cosq34lt1  13182