Theorem 3mix3d

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

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