bitr2i Show Code edit
## Transitive Property
thm (bitr2i () (1 (<-> ph ps) 2 (<-> ps ch)) (<-> ch ph)
1 2 bitri bicomi)
(<-> ch ph)
edit