Theorem syl56

Description: Combine syl5 and syl6 . (Contributed by NM, 14-Nov-2013)

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

Proof

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