Theorem spimed

Deduction version of spime. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) Usage of this theorem is discouraged because it depends on [ax-13]. Use spimedv instead. (New usage is discouraged.)

Hypotheses
spimed.1
\( \vdash \chi \rightarrow \Finv x \, \varphi \)
spimed.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \rightarrow \varphi \rightarrow \exists x \, \psi \)
Proof
spimed.1
l1
nf5rd _
\( \vdash \chi \rightarrow \varphi \rightarrow \forall x \, \varphi \)
l2
ax6e
\( \vdash \exists x \, x = y' \)
spimed.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
eximii l2 _
19.35i _
\( \vdash \forall x \, \varphi \rightarrow \exists x \, \psi \)
syl6 l1 _