Theorem mp3an3an

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

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