Theorem syl1111anc

Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)

Hypotheses
syl1111anc.1
\( \vdash \varphi \rightarrow \psi \)
syl1111anc.2
\( \vdash \varphi \rightarrow \chi \)
syl1111anc.3
\( \vdash \varphi \rightarrow \theta \)
syl1111anc.4
\( \vdash \varphi \rightarrow \tau \)
syl1111anc.5
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \eta \)
Proof
l0
syl1111anc.1
syl1111anc.2
l2
jca l0 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
l3
syl1111anc.3
\( \vdash \varphi \rightarrow \theta \)
l4
syl1111anc.4
\( \vdash \varphi \rightarrow \tau \)
syl1111anc.5
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \rightarrow \eta \)
syl21anc l2 l3 l4 _