Theorem 3jaod

Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)

Hypotheses
3jaod.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3jaod.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
3jaod.3
\( \vdash \varphi \rightarrow \tau \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \tau \rightarrow \chi \)
Proof
l0
3jaod.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
3jaod.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
l2
3jaod.3
\( \vdash \varphi \rightarrow \tau \rightarrow \chi \)
3jao
\( \vdash (\psi \rightarrow \chi) \wedge (\theta \rightarrow \chi) \wedge (\tau \rightarrow \chi) \rightarrow \psi \vee \theta \vee \tau \rightarrow \chi \)
syl3anc l0 l1 l2 _