Theorem 3mix1i

Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)

Hypothesis
3mixi.1
\( \vdash \varphi \)
Conclusion
\( \vdash \varphi \vee \psi \vee \chi \)
Proof
l0
3mixi.1
\( \vdash \varphi \)
3mix1
\( \vdash \varphi \rightarrow \varphi \vee \psi \vee \chi \)
ax-mp l0 _