Theorem eel00001 38948

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

Hypotheses

Ref	Expression
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

Ref	Expression
eel00001	|- ( ta -> ze )

Proof of Theorem eel00001

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

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by: (None)