Theorem ecase13d
Deduction for elimination by cases. (Contributed by Jeff Hankins,
18-Aug-2009.)
Hypotheses
ecase13d.1
\( \vdash \varphi \rightarrow \neg \chi \)
ecase13d.2
\( \vdash \varphi \rightarrow \neg \theta \)
ecase13d.3
\( \vdash \varphi \rightarrow \chi \vee \psi \vee \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
ecase13d.1
\( \vdash \varphi \rightarrow \neg \chi \)
l1
ecase13d.3
\( \vdash \varphi \rightarrow \chi \vee \psi \vee \theta \)
l2
3orass
\( \vdash \chi \vee \psi \vee \theta \leftrightarrow \chi \vee (\psi \vee \theta) \)
df-or
\( \vdash \chi \vee (\psi \vee \theta) \leftrightarrow \neg \chi \rightarrow \psi \vee \theta \)
bitri l2 _
\( \vdash \chi \vee \psi \vee \theta \leftrightarrow \neg \chi \rightarrow \psi \vee \theta \)
sylib l1 _
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \psi \vee \theta \)
l6
mpd l0 _
\( \vdash \varphi \rightarrow \psi \vee \theta \)
ecase13d.2
\( \vdash \varphi \rightarrow \neg \theta \)
olcnd l6 _