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