bitr3d Show Code edit
# Deduction form of [[bitr3i]].
## Transitive Property
thm (bitr3d () (bitr3d.1 (-> ph (<-> ps ch)) bitr3d.2 (-> ph (<-> ps th))) (-> ph (<-> ch th)) bitr3d.1 bicomd bitr3d.2 bitrd)
(-> ph (<-> ch th))
edit