Theorem eel0TT 31783

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 1387	. . . 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 1302	. . . . 5 |- ( ( ps /\ ch ) -> th )
7	3, 6	sylan 471	. . . 4 |- ( ( T. /\ ch ) -> th )
8	2, 7	sylbir 213	. . 3 |- ( ch -> th )
9	1, 8	syl 16	. 2 |- ( T. -> th )
10	9	trud 1379	1 |- th

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   T. wtru 1371

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 371  df-3an 967  df-tru 1373

This theorem is referenced by: (None)