Theorem 3mix3i

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

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