3bitr3i Show Code edit
# This is getting boring...
## Transitive Property
thm (3bitr3i () (1 (<-> ph ps) 2 (<-> ph ch) 3 (<-> ps th)) (<-> ch th)
2 bicomi 1 3 3bitri)
(<-> ch th)
edit