Theorem speiv

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

Hypotheses
speiv.1
\( \vdash x = y' \rightarrow \psi \rightarrow \varphi \)
speiv.2
\( \vdash \psi \)
Conclusion
\( \vdash \exists x \, \varphi \)
Proof
l0
speiv.2
\( \vdash \psi \)
speiv.2
l2
hbth _
\( \vdash \psi \rightarrow \forall x \, \psi \)
speiv.1
\( \vdash x = y' \rightarrow \psi \rightarrow \varphi \)
spimew l2 _
\( \vdash \psi \rightarrow \exists x \, \varphi \)
ax-mp l0 _