Theorem eel0T1

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

	Ref	Expression
Hypotheses	eel0T1.1	|- ph
	eel0T1.2	|- ( T. -> ps )
	eel0T1.3	|- ( ch -> th )
	eel0T1.4	|- ( ( ph /\ ps /\ th ) -> ta )
Assertion	eel0T1	|- ( ch -> ta )

Proof

Step	Hyp	Ref	Expression
1		eel0T1.1	|- ph
2		eel0T1.2	|- ( T. -> ps )
3		eel0T1.3	|- ( ch -> th )
4		eel0T1.4	|- ( ( ph /\ ps /\ th ) -> ta )
5		3anass	|- ( ( ph /\ T. /\ ch ) <-> ( ph /\ ( T. /\ ch ) ) )
6		simpr	|- ( ( ph /\ ( T. /\ ch ) ) -> ( T. /\ ch ) )
7	1	jctl	|- ( ( T. /\ ch ) -> ( ph /\ ( T. /\ ch ) ) )
8	6 7	impbii	|- ( ( ph /\ ( T. /\ ch ) ) <-> ( T. /\ ch ) )
9		truan	|- ( ( T. /\ ch ) <-> ch )
10	5 8 9	3bitri	|- ( ( ph /\ T. /\ ch ) <-> ch )
11	2 4	syl3an2	|- ( ( ph /\ T. /\ th ) -> ta )
12	3 11	syl3an3	|- ( ( ph /\ T. /\ ch ) -> ta )
13	10 12	sylbir	|- ( ch -> ta )