Theorem spimedv

Deduction version of spimev. Version of spimed with a disjoint variable condition, which does not require [ax-13]. See spime for a non-deduction version. (Contributed by NM, 14-May-1993.) (Revised by BJ, 31-May-2019.)

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