Description: Alias for ax-addcl , for naming consistency with addcli . Use this theorem instead of ax-addcl or axaddcl . (Contributed by NM, 10-Mar-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | addcl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-addcl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ ) |