Theorem 3mix1

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

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