Theorem ecase2d
Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Wolf Lammen, 19-Sep-2024.)
Hypotheses
ecase2d.1
\( \vdash \varphi \rightarrow \psi \)
ecase2d.2
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \)
ecase2d.3
\( \vdash \varphi \rightarrow \neg (\psi \wedge \theta) \)
ecase2d.4
\( \vdash \varphi \rightarrow \tau \vee (\chi \vee \theta) \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
ecase2d.1
\( \vdash \varphi \rightarrow \psi \)
ecase2d.2
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \)
l2
mpnanrd l0 _
\( \vdash \varphi \rightarrow \neg \chi \)
l3
ecase2d.1
\( \vdash \varphi \rightarrow \psi \)
ecase2d.3
\( \vdash \varphi \rightarrow \neg (\psi \wedge \theta) \)
l5
mpnanrd l3 _
\( \vdash \varphi \rightarrow \neg \theta \)
ecase2d.4
ord _
\( \vdash \varphi \rightarrow \neg \tau \rightarrow \chi \vee \theta \)
mtord l2 l5 _
notnotrd _