bitri Show Code edit
## Transitive Property
##
## (<-> ph ] [ ps ] ] )
## [ (<-> [ ps ] [ ch)
## (<-> ph ] [ [ [ ch)
##
thm (bitri () (1 (<-> ph ps) 2 (<-> ps ch)) (<-> ph ch)
1 biimpi 2 biimpi syl
(-> ph ch)
2 biimpri 1 biimpri syl
(-> ch ph)
impbii)
(<-> ph ch)
edit