Theorem syl2an2

Description: syl2an with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016)

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

Proof

Step	Hyp	Ref	Expression
1		syl2an2.1	|- ( ph -> ps )
2		syl2an2.2	|- ( ( ch /\ ph ) -> th )
3		syl2an2.3	|- ( ( ps /\ th ) -> ta )
4	1	adantl	|- ( ( ch /\ ph ) -> ps )
5	4 2 3	syl2anc	|- ( ( ch /\ ph ) -> ta )