Theorem 3orel1

Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)

Conclusion
\( \vdash \neg \varphi \rightarrow \varphi \vee \psi \vee \chi \rightarrow \psi \vee \chi \)
Proof
l0
3orass
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee (\psi \vee \chi) \)
orel1
\( \vdash \neg \varphi \rightarrow \varphi \vee (\psi \vee \chi) \rightarrow \psi \vee \chi \)
biimtrid l0 _