pm2.38 Show Code edit
# Theorem *2.38 of [bib/WhiteheadRussell] p. 105.
## Add disjunct to antecedent and consequent
thm (pm2.38 () () (-> (-> ps ch) (-> (\/ ps ph) (\/ ch ph))) (-> ps ch) id ph orim1d)
(-> (-> ps ch) (-> (\/ ps ph) (\/ ch ph)))
edit