Theorem mpjaod

Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses
jaod.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
jaod.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
jaod.3
\( \vdash \varphi \rightarrow \psi \vee \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
jaod.3
\( \vdash \varphi \rightarrow \psi \vee \theta \)
l1
jaod.1
jaod.2
jaod l1 _
\( \vdash \varphi \rightarrow \psi \vee \theta \rightarrow \chi \)
mpd l0 _