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