orim2 Show Code edit
# Axiom *1.6 (Sum) of [bib/WhiteheadRussell] p. 97.
## Add disjunct to antecedent and consequent
thm (orim2 () () (-> (-> ps ch) (-> (\/ ph ps) (\/ ph ch))) (-> ps ch) id ph orim2d)
(-> (-> ps ch) (-> (\/ ph ps) (\/ ph ch)))
edit