Metamath Proof Explorer


Theorem eel132

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

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

Proof

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