Theorem mulcli 7975

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

Syntax hints:   ∈ wcel 2158  (class class class)co 5888  ℂcc 7822   · cmul 7829

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

This theorem is referenced by:  ixi  8553  2mulicn  9154  numma  9440  nummac  9441  9t11e99  9526  decbin2  9537  irec  10633  binom2i  10642  3dec  10707  rei  10921  imi  10922  3dvdsdec  11883  3dvds2dec  11884  odd2np1  11891  3lcm2e6woprm  12099  6lcm4e12  12100  sinhalfpilem  14483  ef2pi  14497  ef2kpi  14498  efper  14499  sinperlem  14500  sin2kpi  14503  cos2kpi  14504  sin2pim  14505  cos2pim  14506  sincos4thpi  14532  sincos6thpi  14534  abssinper  14538  cosq34lt1  14542  lgsdir2lem5  14704  2lgsoddprmlem3c  14728  2lgsoddprmlem3d  14729