Theorem mp3an1

An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses
mp3an1.1
\( \vdash \varphi \)
mp3an1.2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Proof
l0
mp3an1.1
\( \vdash \varphi \)
mp3an1.2
3expb _
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
mpan l0 _