$( <MM> <PROOF ASST> THEOREM= syllogism  LOC_AFTER= syllogism
 
h1::            |- (ph -> ps)
h2::            |- (ps -> ch)
3:2:            |- (ph -> (ps -> ch))
4:3:            |- ((ph -> ps) -> (ph -> ch))
qed:1,4:        |- (ph -> ch)

$)