Theorem 3ori

Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)

Hypothesis
3ori.1
\( \vdash \varphi \vee \psi \vee \chi \)
Conclusion
\( \vdash \neg \varphi \wedge \neg \psi \rightarrow \chi \)
Proof
l0
ioran
\( \vdash \neg (\varphi \vee \psi) \leftrightarrow \neg \varphi \wedge \neg \psi \)
l1
3ori.1
\( \vdash \varphi \vee \psi \vee \chi \)
df-3or
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \psi \vee \chi \)
mpbi l1 _
ori _
\( \vdash \neg (\varphi \vee \psi) \rightarrow \chi \)
sylbir l0 _