Theorem syl6c

Description: Inference combining syl6 with contraction. (Contributed by Alan Sare, 2-May-2011)

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

Proof

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