Theorem ee101

Description: e101 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ee101.1	|- ( ph -> ps )
	ee101.2	|- ch
	ee101.3	|- ( ph -> th )
	ee101.4	|- ( ps -> ( ch -> ( th -> ta ) ) )
Assertion	ee101	|- ( ph -> ta )

Proof

Step	Hyp	Ref	Expression
1		ee101.1	|- ( ph -> ps )
2		ee101.2	|- ch
3		ee101.3	|- ( ph -> th )
4		ee101.4	|- ( ps -> ( ch -> ( th -> ta ) ) )
5	2	a1i	|- ( ph -> ch )
6	1 5 3 4	syl3c	|- ( ph -> ta )