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