Theorem exlimdv

Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23. (Contributed by NM, 27-Apr-1994.) Remove dependencies on [ax-6], [ax-7]. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis
exlimdv.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \chi \)
Proof
exlimdv.1
l1
eximdv _
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \exists x \, \chi \)
ax5e
\( \vdash \exists x \, \chi \rightarrow \chi \)
syl6 l1 _