Theorem mpjaodan

Eliminate a disjunction in a deduction. A translation of natural deduction rule \/ E ( \/ elimination), see [natded]. (Contributed by Mario Carneiro, 29-May-2016.)

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