Theorem syl6an

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		syl6an.1	|- ( ph -> ps )
2		syl6an.2	|- ( ph -> ( ch -> th ) )
3		syl6an.3	|- ( ( ps /\ th ) -> ta )
4	3	ex	|- ( ps -> ( th -> ta ) )
5	1 2 4	sylsyld	|- ( ph -> ( ch -> ta ) )