pm3.27 Show Code edit
# Elimination of a conjunct. Theorem *3.27 (Simp) of [bib/WhiteheadRussell]
# p. 112.
## Remove Left Side of AND
thm (pm3.27 () () (-> (/\ ph ps) ps) ph ps df-an ph ps pm3.27im sylbi)
(-> (/\ ph ps) ps)
edit