Theorem pm2.61ddan

Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)

Hypotheses
pm2.61ddan.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
pm2.61ddan.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
pm2.61ddan.3
\( \vdash \varphi \wedge (\neg \psi \wedge \neg \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
pm2.61ddan.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
pm2.61ddan.2
l2
adantlr _
\( \vdash \varphi \wedge \neg \psi \wedge \chi \rightarrow \theta \)
pm2.61ddan.3
anassrs _
\( \vdash \varphi \wedge \neg \psi \wedge \neg \chi \rightarrow \theta \)
pm2.61dan l2 _
\( \vdash \varphi \wedge \neg \psi \rightarrow \theta \)
pm2.61dan l0 _