Theorem exlimdd

Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened 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 \)
exlimdd.4
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
exlimdd.1
\( \vdash \Finv x \, \varphi \)
l1
exlimdd.2
\( \vdash \Finv x \, \chi \)
l2
exlimdd.3
\( \vdash \varphi \rightarrow \exists x \, \psi \)
exlimdd.4
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
exlimimdd l0 l1 l2 _