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