Theorem syl2an2r

Description: syl2anr with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016) (Proof shortened by Wolf Lammen, 28-Mar-2022)

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

Proof

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