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	|- ( ch -> F/ x ps )
	spd.2	|- ( x = y -> ( ph <-> ps ) )
Assertion	spd	|- ( ch -> ( A. x ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		spd.1	|- ( ch -> F/ x ps )
2		spd.2	|- ( x = y -> ( ph <-> ps ) )
3		ax6e	|- E. x x = y
4	2	biimpd	|- ( x = y -> ( ph -> ps ) )
5	3 4	eximii	|- E. x ( ph -> ps )
6	5	19.35i	|- ( A. x ph -> E. x ps )
7	1	19.9d	|- ( ch -> ( E. x ps -> ps ) )
8	6 7	syl5	|- ( ch -> ( A. x ph -> ps ) )