Theorem exlimddv

Existential elimination rule of natural deduction (Rule C, explained in exlimiv ). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses
exlimddv.1
\( \vdash \varphi \rightarrow \exists x \, \psi \)
exlimddv.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
exlimddv.1
\( \vdash \varphi \rightarrow \exists x \, \psi \)
exlimddv.2
ex _
exlimdv _
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \chi \)
mpd l0 _