Theorem mpsyl4anc

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

Hypotheses
mpsyl4anc.1
\( \vdash \varphi \)
mpsyl4anc.2
\( \vdash \psi \)
mpsyl4anc.3
\( \vdash \chi \)
mpsyl4anc.4
\( \vdash \theta \rightarrow \tau \)
mpsyl4anc.5
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \theta \rightarrow \eta \)
Proof
mpsyl4anc.1
l1
a1i _
\( \vdash \theta \rightarrow \varphi \)
mpsyl4anc.2
l3
a1i _
\( \vdash \theta \rightarrow \psi \)
mpsyl4anc.3
l5
a1i _
\( \vdash \theta \rightarrow \chi \)
l6
mpsyl4anc.4
\( \vdash \theta \rightarrow \tau \)
mpsyl4anc.5
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \tau \rightarrow \eta \)
syl1111anc l1 l3 l5 l6 _