Theorem mpjao3dan

Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.)

Hypotheses
mpjao3dan.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
mpjao3dan.2
\( \vdash \varphi \wedge \theta \rightarrow \chi \)
mpjao3dan.3
\( \vdash \varphi \wedge \tau \rightarrow \chi \)
mpjao3dan.4
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \tau \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
mpjao3dan.4
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \tau \)
l1
mpjao3dan.1
l2
mpjao3dan.2
mpjao3dan.3
3jaodan l1 l2 _
\( \vdash \varphi \wedge (\psi \vee \theta \vee \tau) \rightarrow \chi \)
mpdan l0 _