imbi12i Show Code edit
## Join two equivalences to form equivalent implication
thm (imbi12i () (1 (<-> ph ps) 2 (<-> ch th)) (<-> (-> ph ch) (-> ps th))
1 ch imbi1i
(<-> (-> ph ch) (-> ps ch))
2 ps imbi2i
(<-> (-> ps ch) (-> ps th))
bitri)
(<-> (-> ph ch) (-> ps th))
edit