Theorem
3orel13
Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
Conclusion
\( \vdash \neg \varphi \wedge \neg \chi \rightarrow \varphi \vee \psi \vee \chi \rightarrow \psi \)
Proof
l0
3orel3
\( \vdash \neg \chi \rightarrow \varphi \vee \psi \vee \chi \rightarrow \varphi \vee \psi \)
orel1
\( \vdash \neg \varphi \rightarrow \varphi \vee \psi \rightarrow \psi \)
sylan9r
l0
_
This is the content in the right pane.