Theorem 3orel3

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

Conclusion
\( \vdash \neg \chi \rightarrow \varphi \vee \psi \vee \chi \rightarrow \varphi \vee \psi \)
Proof
l0
df-3or
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \psi \vee \chi \)
orel2
\( \vdash \neg \chi \rightarrow \varphi \vee \psi \vee \chi \rightarrow \varphi \vee \psi \)
biimtrid l0 _