Theorem syldanl

Description: A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011)

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

Proof

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