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