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