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