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	⊢ ( 𝜒 → Ⅎ 𝑥 𝜓 )
	spd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	spd	⊢ ( 𝜒 → ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		spd.1	⊢ ( 𝜒 → Ⅎ 𝑥 𝜓 )
2		spd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
4	2	biimpd	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
5	3 4	eximii	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
6	5	19.35i	⊢ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 )
7	1	19.9d	⊢ ( 𝜒 → ( ∃ 𝑥 𝜓 → 𝜓 ) )
8	6 7	syl5	⊢ ( 𝜒 → ( ∀ 𝑥 𝜑 → 𝜓 ) )