Theorem 3mix2

Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Conclusion
\( \vdash \varphi \rightarrow \psi \vee \varphi \vee \chi \)
Proof
l0
3mix1
\( \vdash \varphi \rightarrow \varphi \vee \chi \vee \psi \)
3orrot
\( \vdash \psi \vee \varphi \vee \chi \leftrightarrow \varphi \vee \chi \vee \psi \)
sylibr l0 _