Theorem mp3an2ani

An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)

Hypotheses
mp3an2ani.1
\( \vdash \varphi \)
mp3an2ani.2
\( \vdash \psi \rightarrow \chi \)
mp3an2ani.3
\( \vdash \psi \wedge \theta \rightarrow \tau \)
mp3an2ani.4
\( \vdash \varphi \wedge \chi \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \psi \wedge \theta \rightarrow \eta \)
Proof
l0
mp3an2ani.1
\( \vdash \varphi \)
l1
mp3an2ani.2
\( \vdash \psi \rightarrow \chi \)
l2
mp3an2ani.3
\( \vdash \psi \wedge \theta \rightarrow \tau \)
mp3an2ani.4
\( \vdash \varphi \wedge \chi \wedge \tau \rightarrow \eta \)
mp3an3an l0 l1 l2 _
anabss5 _