Theorem eximd

Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypotheses
eximd.1
\( \vdash \Finv x \, \varphi \)
eximd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \exists x \, \chi \)
Proof
eximd.1
l1
nf5ri _
eximd.2
eximdh l1 _