impbid2 Show Code edit
## Infer Biconditional from two conditionals
thm (impbid2 () (impbid2.1 (-> ps ch) impbid2.2 (-> ph (-> ch ps))) (-> ph (<-> ps ch)) impbid2.1 ph a1i impbid2.2 impbid)
(-> ph (<-> ps ch))
edit