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