pm3.27bda Show Code edit
## Deduction eliminating a conjunct
thm (pm3.27bda () (pm3.26bda.1 (-> ph (<-> ps (/\ ch th)))) (-> (/\ ph ps) th) pm3.26bda.1 biimpa pm3.27d)
(-> (/\ ph ps) th)
edit