pm2.81 Show Code edit
# Theorem *2.81 of [bib/WhiteheadRussell] p. 108.
thm (pm2.81 () () (-> (-> ps (-> ch th)) (-> (\/ ph ps) (-> (\/ ph ch) (\/ ph th)))) ps (-> ch th) ph orim2 ph ch th pm2.76 syl6)
(-> (-> ps (-> ch th)) (-> (\/ ph ps) (-> (\/ ph ch) (\/ ph th))))
edit