Theorem eel11111

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

	Ref	Expression
Hypotheses	eel11111.1	|- ( ph -> ps )
	eel11111.2	|- ( ph -> ch )
	eel11111.3	|- ( ph -> th )
	eel11111.4	|- ( ph -> ta )
	eel11111.5	|- ( ph -> et )
	eel11111.6	|- ( ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze )
Assertion	eel11111	|- ( ph -> ze )

Proof

Step	Hyp	Ref	Expression
1		eel11111.1	|- ( ph -> ps )
2		eel11111.2	|- ( ph -> ch )
3		eel11111.3	|- ( ph -> th )
4		eel11111.4	|- ( ph -> ta )
5		eel11111.5	|- ( ph -> et )
6		eel11111.6	|- ( ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze )
7	6	exp41	|- ( ( ps /\ ch ) -> ( th -> ( ta -> ( et -> ze ) ) ) )
8	7	ex	|- ( ps -> ( ch -> ( th -> ( ta -> ( et -> ze ) ) ) ) )
9	1 2 3 8	syl3c	|- ( ph -> ( ta -> ( et -> ze ) ) )
10	4 5 9	mp2d	|- ( ph -> ze )