Theorem exlimimdd

Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd. (Revised by Wolf Lammen, 3-Sep-2023.)

Hypotheses
exlimdd.1
\( \vdash \Finv x \, \varphi \)
exlimdd.2
\( \vdash \Finv x \, \chi \)
exlimdd.3
\( \vdash \varphi \rightarrow \exists x \, \psi \)
exlimimdd.4
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
exlimdd.3
\( \vdash \varphi \rightarrow \exists x \, \psi \)
l1
exlimdd.1
l2
exlimdd.2
exlimimdd.4
exlimd l1 l2 _
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \chi \)
mpd l0 _