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