Theorem eel3132

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

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

Proof

Step	Hyp	Ref	Expression
1		eel3132.1	|- ( ( ph /\ ps ) -> ch )
2		eel3132.2	|- ( ( th /\ ps ) -> ta )
3		eel3132.3	|- ( ( ch /\ ta ) -> et )
4	1 2 3	syl2an	|- ( ( ( ph /\ ps ) /\ ( th /\ ps ) ) -> et )
5	4	3impdir	|- ( ( ph /\ th /\ ps ) -> et )