pm2.46 Show Code edit
# Theorem *2.46 of [bib/WhiteheadRussell] p. 106.
## Eliminate a Disjunct
thm (pm2.46 () () (-> (-. (\/ ph ps)) (-. ps)) ps ph olc con3i)
(-> (-. (\/ ph ps)) (-. ps))
edit