bitrd Show Code edit
# Deduction form of [[bitri]].
## Transitive Property
thm (bitrd () (bitrd.1 (-> ph (<-> ps ch)) bitrd.2 (-> ph (<-> ch th))) (-> ph (<-> ps th)) bitrd.1 biimpd bitrd.2 sylibd bitrd.2 biimprd bitrd.1 sylibrd impbid)
(-> ph (<-> ps th))
edit