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	|- ( ph -> ps )
	syl1111anc.2	|- ( ph -> ch )
	syl1111anc.3	|- ( ph -> th )
	syl1111anc.4	|- ( ph -> ta )
	syl1111anc.5	|- ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) -> et )
Assertion	syl1111anc	|- ( ph -> et )

Proof

Step	Hyp	Ref	Expression
1		syl1111anc.1	|- ( ph -> ps )
2		syl1111anc.2	|- ( ph -> ch )
3		syl1111anc.3	|- ( ph -> th )
4		syl1111anc.4	|- ( ph -> ta )
5		syl1111anc.5	|- ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) -> et )
6	1 2	jca	|- ( ph -> ( ps /\ ch ) )
7	6 3 4 5	syl21anc	|- ( ph -> et )