biimpar Show Code edit
## Inference from logical equivalence
thm (biimpar () (biimpa.1 (-> ph (<-> ps ch))) (-> (/\ ph ch) ps) biimpa.1 biimprd imp)
(-> (/\ ph ch) ps)
edit