sylib Show Code edit
## Syllogism
##
## (-> ph [ ps ] ] ] )
## [ (<-> ps ] [ ch ] )
## (-> ph [ [ [ ch ] )
##
thm (sylib () (1 (-> ph ps) 2 (<-> ps ch)) (-> ph ch)
1 2 biimpi syl)
(-> ph ch)
edit