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