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