syl Show Code edit
## Syllogism
##
## (-> ph [ ps ] ] ] )
## [ (-> ps ] [ ch ] )
## (-> ph [ [ [ ch ] )
##
thm (syl () (1 (-> ph ps) 2 (-> ps ch)) (-> ph ch)
1 2 ph a1i a2i ax-mp)
(-> ph ch)
edit