Metamath Proof Explorer


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 )