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