Theorem spesbcd

Description: form of spsbc . (Contributed by Mario Carneiro, 9-Feb-2017)

	Ref	Expression
Hypothesis	spesbcd.1	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
Assertion	spesbcd	$$⊢\phi \to \exists x\psi$$

Proof

Step	Hyp	Ref	Expression
1		spesbcd.1	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
2		spesbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \to \exists x\psi$$
3	1 2	syl	$$⊢\phi \to \exists x\psi$$