Theorem eel2131

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

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

Proof

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