Theorem 3orel2

Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Eric Schmidt, 8-Oct-2025.)

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