Description: Alias for ax-mulcl , for naming consistency with mulcli . (Contributed by NM, 10-Mar-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | mulcl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ ) |