Theorem eel00001

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

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