Theorem spd

Description: Specialization deduction, using implicit substitution. Based on the proof of spimed . (Contributed by Emmett Weisz, 17-Jan-2020)

	Ref	Expression
Hypotheses	spd.1	$$⊢\chi \to Ⅎx\psi$$
	spd.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spd	$$⊢\chi \to \left(\forall x\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spd.1	$$⊢\chi \to Ⅎx\psi$$
2		spd.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		ax6e	$$⊢\exists xx=y$$
4	2	biimpd	$$⊢x=y\to \left(\phi \to \psi \right)$$
5	3 4	eximii	$$⊢\exists x\left(\phi \to \psi \right)$$
6	5	19.35i	$$⊢\forall x\phi \to \exists x\psi$$
7	1	19.9d	$$⊢\chi \to \left(\exists x\psi \to \psi \right)$$
8	6 7	syl5	$$⊢\chi \to \left(\forall x\phi \to \psi \right)$$