Theorem eel0TT 36497

Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
eel0TT.1	|- ph
eel0TT.2	|- ( T. -> ps )
eel0TT.3	|- ( T. -> ch )
eel0TT.4	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
eel0TT	|- th

Proof of Theorem eel0TT

Step	Hyp	Ref	Expression
1		eel0TT.3	. . 3 |- ( T. -> ch )
2		truan 1422	. . . 4 |- ( ( T. /\ ch ) <-> ch )
3		eel0TT.2	. . . . 5 |- ( T. -> ps )
4		eel0TT.1	. . . . . 6 |- ph
5		eel0TT.4	. . . . . 6 |- ( ( ph /\ ps /\ ch ) -> th )
6	4, 5	mp3an1 1313	. . . . 5 |- ( ( ps /\ ch ) -> th )
7	3, 6	sylan 469	. . . 4 |- ( ( T. /\ ch ) -> th )
8	2, 7	sylbir 213	. . 3 |- ( ch -> th )
9	1, 8	syl 17	. 2 |- ( T. -> th )
10	9	trud 1414	1 |- th

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974   T. wtru 1406

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 185  df-an 369  df-3an 976  df-tru 1408

This theorem is referenced by: (None)