Theorem 3mix2i

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

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