Theorem syl1111anc

Description: 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)

	Ref	Expression
Hypotheses	syl1111anc.1	$$⊢\phi \to \psi$$
	syl1111anc.2	$$⊢\phi \to \chi$$
	syl1111anc.3	$$⊢\phi \to \theta$$
	syl1111anc.4	$$⊢\phi \to \tau$$
	syl1111anc.5	$$⊢\left(\left(\left(\psi \wedge \chi \right)\wedge \theta \right)\wedge \tau \right)\to \eta$$
Assertion	syl1111anc	$$⊢\phi \to \eta$$

Proof

Step	Hyp	Ref	Expression
1		syl1111anc.1	$$⊢\phi \to \psi$$
2		syl1111anc.2	$$⊢\phi \to \chi$$
3		syl1111anc.3	$$⊢\phi \to \theta$$
4		syl1111anc.4	$$⊢\phi \to \tau$$
5		syl1111anc.5	$$⊢\left(\left(\left(\psi \wedge \chi \right)\wedge \theta \right)\wedge \tau \right)\to \eta$$
6	1 2	jca	$$⊢\phi \to \left(\psi \wedge \chi \right)$$
7	6 3 4 5	syl21anc	$$⊢\phi \to \eta$$