Theorem mp4an

An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)

Hypotheses
mp4an.1
\( \vdash \varphi \)
mp4an.2
\( \vdash \psi \)
mp4an.3
\( \vdash \chi \)
mp4an.4
\( \vdash \theta \)
mp4an.5
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \tau \)
Proof
l0
mp4an.1
mp4an.2
l2
pm3.2i l0 _
\( \vdash \varphi \wedge \psi \)
l3
mp4an.3
mp4an.4
l5
pm3.2i l3 _
\( \vdash \chi \wedge \theta \)
mp4an.5
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
mp2an l2 l5 _