Metamath Proof Explorer

Theorem rpefcld

Description: The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis rpefcld.1 φ A
Assertion rpefcld φ e A +


Step Hyp Ref Expression
1 rpefcld.1 φ A
2 rpefcl A e A +
3 1 2 syl φ e A +