Metamath Proof Explorer


Theorem sylani

Description: A syllogism inference. (Contributed by NM, 2-May-1996)

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

Proof

Step Hyp Ref Expression
1 sylani.1
 |-  ( ph -> ch )
2 sylani.2
 |-  ( ps -> ( ( ch /\ th ) -> ta ) )
3 1 a1i
 |-  ( ps -> ( ph -> ch ) )
4 3 2 syland
 |-  ( ps -> ( ( ph /\ th ) -> ta ) )