Theorem mp3an1i

An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)

Hypotheses
mp3an1i.1
\( \vdash \psi \)
mp3an1i.2
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \chi \wedge \theta \rightarrow \tau \)
Proof
l0
mp3an1i.1
\( \vdash \psi \)
mp3an1i.2
com12 _
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \varphi \rightarrow \tau \)
mp3an1 l0 _
com12 _