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