Metamath Proof Explorer


Theorem mulcli

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994)

Ref Expression
Hypotheses axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
Assertion mulcli ( 𝐴 · 𝐵 ) ∈ ℂ

Proof

Step Hyp Ref Expression
1 axi.1 𝐴 ∈ ℂ
2 axi.2 𝐵 ∈ ℂ
3 mulcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
4 1 2 3 mp2an ( 𝐴 · 𝐵 ) ∈ ℂ