Theorem ecase23d
Deduction for elimination by cases. (Contributed by NM,
22-Apr-1994.)
Hypotheses
ecase23d.1
\( \vdash \varphi \rightarrow \neg \chi \)
ecase23d.2
\( \vdash \varphi \rightarrow \neg \theta \)
ecase23d.3
\( \vdash \varphi \rightarrow \psi \vee \chi \vee \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
ecase23d.3
\( \vdash \varphi \rightarrow \psi \vee \chi \vee \theta \)
3orass
\( \vdash \psi \vee \chi \vee \theta \leftrightarrow \psi \vee (\chi \vee \theta) \)
l2
sylib l0 _
\( \vdash \varphi \rightarrow \psi \vee (\chi \vee \theta) \)
l3
ecase23d.1
\( \vdash \varphi \rightarrow \neg \chi \)
l4
ecase23d.2
\( \vdash \varphi \rightarrow \neg \theta \)
ioran
\( \vdash \neg (\chi \vee \theta) \leftrightarrow \neg \chi \wedge \neg \theta \)
sylanbrc l3 l4 _
\( \vdash \varphi \rightarrow \neg (\chi \vee \theta) \)
olcnd l2 _