Theorem mp3an12i

mp3an with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses
mp3an12i.1
\( \vdash \varphi \)
mp3an12i.2
\( \vdash \psi \)
mp3an12i.3
\( \vdash \chi \rightarrow \theta \)
mp3an12i.4
\( \vdash \varphi \wedge \psi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \chi \rightarrow \tau \)
Proof
l0
mp3an12i.3
\( \vdash \chi \rightarrow \theta \)
l1
mp3an12i.1
\( \vdash \varphi \)
l2
mp3an12i.2
\( \vdash \psi \)
mp3an12i.4
\( \vdash \varphi \wedge \psi \wedge \theta \rightarrow \tau \)
mp3an12 l1 l2 _
\( \vdash \theta \rightarrow \tau \)
syl l0 _