Theorem mp3an2

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

Hypotheses
mp3an2.1
\( \vdash \psi \)
mp3an2.2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Proof
l0
mp3an2.1
\( \vdash \psi \)
mp3an2.2
3expa _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpanl2 l0 _