pm2.76 Show Code edit
# Theorem *2.76 of [bib/WhiteheadRussell] p. 108.
thm (pm2.76 () () (-> (\/ ph (-> ps ch)) (-> (\/ ph ps) (\/ ph ch))) ph ps ch pm2.75 com12)
(-> (\/ ph (-> ps ch)) (-> (\/ ph ps) (\/ ph ch)))
edit