pm3.26i Show Code edit
# Inference eliminating a conjunct.
## 'Remove Right Side of AND'
thm (pm3.26i () (pm3.26i.1 (/\ ph ps)) ph pm3.26i.1 ph ps pm3.26 ax-mp)
ph
edit