Theorem speiv

Description: Inference from existential specialization. (Contributed by NM, 19-Aug-1993) (Revised by Wolf Lammen, 22-Oct-2023)

	Ref	Expression
Hypotheses	speiv.1	$$⊢x=y\to \left(\psi \to \phi \right)$$
	speiv.2	$$⊢\psi$$
Assertion	speiv	$$⊢\exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		speiv.1	$$⊢x=y\to \left(\psi \to \phi \right)$$
2		speiv.2	$$⊢\psi$$
3	2	hbth	$$⊢\psi \to \forall x\psi$$
4	3 1	spimew	$$⊢\psi \to \exists x\phi$$
5	2 4	ax-mp	$$⊢\exists x\phi$$