Theorem mp3an2i

mp3an with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses
mp3an2i.1
\( \vdash \varphi \)
mp3an2i.2
\( \vdash \psi \rightarrow \chi \)
mp3an2i.3
\( \vdash \psi \rightarrow \theta \)
mp3an2i.4
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \psi \rightarrow \tau \)
Proof
l0
mp3an2i.2
\( \vdash \psi \rightarrow \chi \)
l1
mp3an2i.3
\( \vdash \psi \rightarrow \theta \)
l2
mp3an2i.1
\( \vdash \varphi \)
mp3an2i.4
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
mp3an1 l2 _
\( \vdash \chi \wedge \theta \rightarrow \tau \)
syl2anc l0 l1 _