Theorem ecase33d
Deduction for elimination by cases. (Contributed by Thierry Arnoux,
5-Jul-2026.)
Hypotheses
ecase33d.1
\( \vdash \varphi \rightarrow \neg \psi \)
ecase33d.2
\( \vdash \varphi \rightarrow \neg \chi \)
ecase33d.3
\( \vdash \varphi \rightarrow \psi \vee \chi \vee \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
ecase33d.3
\( \vdash \varphi \rightarrow \psi \vee \chi \vee \theta \)
df-3or
\( \vdash \psi \vee \chi \vee \theta \leftrightarrow \psi \vee \chi \vee \theta \)
l2
sylib l0 _
\( \vdash \varphi \rightarrow \psi \vee \chi \vee \theta \)
l3
ecase33d.1
\( \vdash \varphi \rightarrow \neg \psi \)
l4
ecase33d.2
\( \vdash \varphi \rightarrow \neg \chi \)
ioran
\( \vdash \neg (\psi \vee \chi) \leftrightarrow \neg \psi \wedge \neg \chi \)
sylanbrc l3 l4 _
\( \vdash \varphi \rightarrow \neg (\psi \vee \chi) \)
orcnd l2 _