Theorem mulcli 7982

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

Syntax hints:   ∈ wcel 2160  (class class class)co 5892  ℂcc 7829   · cmul 7836

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

This theorem is referenced by:  ixi  8560  2mulicn  9161  numma  9447  nummac  9448  9t11e99  9533  decbin2  9544  irec  10640  binom2i  10649  3dec  10714  rei  10928  imi  10929  3dvdsdec  11890  3dvds2dec  11891  odd2np1  11898  3lcm2e6woprm  12106  6lcm4e12  12107  sinhalfpilem  14616  ef2pi  14630  ef2kpi  14631  efper  14632  sinperlem  14633  sin2kpi  14636  cos2kpi  14637  sin2pim  14638  cos2pim  14639  sincos4thpi  14665  sincos6thpi  14667  abssinper  14671  cosq34lt1  14675  lgsdir2lem5  14837  2lgsoddprmlem3c  14861  2lgsoddprmlem3d  14862