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