Metamath Proof Explorer


Theorem efcld

Description: Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypothesis efcld.1 ( 𝜑𝐴 ∈ ℂ )
Assertion efcld ( 𝜑 → ( exp ‘ 𝐴 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 efcld.1 ( 𝜑𝐴 ∈ ℂ )
2 efcl ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
3 1 2 syl ( 𝜑 → ( exp ‘ 𝐴 ) ∈ ℂ )