Metamath Proof Explorer

Theorem cxpcld

Description: Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses cxp0d.1 φ A
cxpcld.2 φ B
Assertion cxpcld φ A B


Step Hyp Ref Expression
1 cxp0d.1 φ A
2 cxpcld.2 φ B
3 cxpcl A B A B
4 1 2 3 syl2anc φ A B