Theorem ecase3ad

Deduction for elimination by cases. (Contributed by NM, 24-May-2013.) (Proof shortened by Wolf Lammen, 20-Sep-2024.)

Hypotheses
ecase3ad.1
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
ecase3ad.2
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
ecase3ad.3
\( \vdash \varphi \rightarrow \neg \psi \wedge \neg \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
ecase3ad.1
l1
imp _
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
ecase3ad.2
l3
imp _
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
ecase3ad.3
imp _
\( \vdash \varphi \wedge (\neg \psi \wedge \neg \chi) \rightarrow \theta \)
pm2.61ddan l1 l3 _