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