Theorem pm2.61dda

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

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