Theorem mp3an3

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

Hypotheses
mp3an3.1
\( \vdash \chi \)
mp3an3.2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
l0
mp3an3.1
\( \vdash \chi \)
mp3an3.2
3expia _
\( \vdash \varphi \wedge \psi \rightarrow \chi \rightarrow \theta \)
mpi l0 _