impbida Show Code edit
# Deduce an equivalence from two implications.
## Deduce Biconditional from two conditionals
thm (impbida () (impbida.1 (-> (/\ ph ps) ch) impbida.2 (-> (/\ ph ch) ps)) (-> ph (<-> ps ch)) impbida.1 ex impbida.2 ex impbid)
(-> ph (<-> ps ch))
edit