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