pm3.27d Show Code edit
# Deduction eliminating a conjunct.
## Remove Left Side of AND
thm (pm3.27d () (pm3.27d.1 (-> ph (/\ ps ch))) (-> ph ch) pm3.27d.1 ps ch pm3.27 syl)
(-> ph ch)
edit