Theorem jaodan

Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses
jaodan.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
jaodan.2
\( \vdash \varphi \wedge \theta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge (\psi \vee \theta) \rightarrow \chi \)
Proof
jaodan.1
l1
ex _
jaodan.2
ex _
jaod l1 _
imp _