Theorem syl10

Description: A nested syllogism inference. (Contributed by Alan Sare, 17-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		syl10.1	|- ( ph -> ( ps -> ch ) )
2		syl10.2	|- ( ph -> ( ps -> ( th -> ta ) ) )
3		syl10.3	|- ( ch -> ( ta -> et ) )
4	1 3	syl6	|- ( ph -> ( ps -> ( ta -> et ) ) )
5	2 4	syldd	|- ( ph -> ( ps -> ( th -> et ) ) )