pm3.26 Show Code edit
# Elimination of a conjunct. Theorem *3.26 (Simp) of [bib/WhiteheadRussell]
# p. 112.
## 'Remove Right Side of AND'
## right('Remove', 'L')
thm (pm3.26 () () (-> (/\ ph ps) ph) ph ps df-an ph ps pm3.26im sylbi)
(-> (/\ ph ps) ph)
edit