pm2.67 Show Code edit
# Theorem *2.67 of [bib/WhiteheadRussell] p. 107.
## Eliminate a Disjunct
thm (pm2.67 () () (-> (-> (\/ ph ps) ps) (-> ph ps)) ph ps orc ps imim1i)
(-> (-> (\/ ph ps) ps) (-> ph ps))
edit