Metamath Proof Explorer


Theorem syl2an2

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

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

Proof

Step Hyp Ref Expression
1 syl2an2.1
 |-  ( ph -> ps )
2 syl2an2.2
 |-  ( ( ch /\ ph ) -> th )
3 syl2an2.3
 |-  ( ( ps /\ th ) -> ta )
4 1 adantl
 |-  ( ( ch /\ ph ) -> ps )
5 4 2 3 syl2anc
 |-  ( ( ch /\ ph ) -> ta )