Theorem 3mix2d

Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis
3mixd.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \vee \psi \vee \theta \)
Proof
l0
3mixd.1
\( \vdash \varphi \rightarrow \psi \)
3mix2
\( \vdash \psi \rightarrow \chi \vee \psi \vee \theta \)
syl l0 _