Theorem 3jaodan

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

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