Theorem sbcthdv

Description: Deduction version of sbcth . (Contributed by NM, 30-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypothesis	sbcthdv.1	$$⊢\phi \to \psi$$
Assertion	sbcthdv	$$⊢\left(\phi \wedge A\in V\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbcthdv.1	$$⊢\phi \to \psi$$
2	1	alrimiv	$$⊢\phi \to \forall x\psi$$
3		spsbc	$$⊢A\in V\to \left(\forall x\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
4	2 3	mpan9	$$⊢\left(\phi \wedge A\in V\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$