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