Theorem eel00000

Description: Elimination rule similar eel0000 , except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eel00000.1	|- ph
2		eel00000.2	|- ps
3		eel00000.3	|- ch
4		eel00000.4	|- th
5		eel00000.5	|- ta
6		eel00000.6	|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> et )
7	6	exp41	|- ( ( ph /\ ps ) -> ( ch -> ( th -> ( ta -> et ) ) ) )
8	1 7	mpan	|- ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) )
9	2 3 8	mp2	|- ( th -> ( ta -> et ) )
10	4 5 9	mp2	|- et