imbi12d Show Code edit
# Deduction joining two equivalences to form equivalence of
# implications.
## Join two equivalences into equivalent implication
thm (imbi12d () (bi12d.1 (-> ph (<-> ps ch)) bi12d.2 (-> ph (<-> th ta))) (-> ph (<-> (-> ps th) (-> ch ta))) bi12d.1 th imbi1d bi12d.2 ch imbi2d bitrd)
(-> ph (<-> (-> ps th) (-> ch ta)))
edit