Metamath Proof Explorer

Theorem nnexpcld

Description: Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses nnexpcld.1 φ A
nnexpcld.2 φ N 0
Assertion nnexpcld φ A N


Step Hyp Ref Expression
1 nnexpcld.1 φ A
2 nnexpcld.2 φ N 0
3 nnexpcl A N 0 A N
4 1 2 3 syl2anc φ A N