Theorem 3mix3

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

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