Theorem mulcli 7957

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

Syntax hints:   ∈ wcel 2148  (class class class)co 5870  ℂcc 7804   · cmul 7811

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

This theorem is referenced by:  ixi  8534  2mulicn  9135  numma  9421  nummac  9422  9t11e99  9507  decbin2  9518  irec  10612  binom2i  10621  3dec  10685  rei  10899  imi  10900  3dvdsdec  11860  3dvds2dec  11861  odd2np1  11868  3lcm2e6woprm  12076  6lcm4e12  12077  sinhalfpilem  13994  ef2pi  14008  ef2kpi  14009  efper  14010  sinperlem  14011  sin2kpi  14014  cos2kpi  14015  sin2pim  14016  cos2pim  14017  sincos4thpi  14043  sincos6thpi  14045  abssinper  14049  cosq34lt1  14053  lgsdir2lem5  14215