Theorem exlimd

Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)

Hypotheses
exlimd.1
\( \vdash \Finv x \, \varphi \)
exlimd.2
\( \vdash \Finv x \, \chi \)
exlimd.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \chi \)
Proof
l0
exlimd.1
exlimd.3
l2
eximd l0 _
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \exists x \, \chi \)
exlimd.2
19.9 _
\( \vdash \exists x \, \chi \leftrightarrow \chi \)
imbitrdi l2 _