pm2.8 Show Code edit
# Theorem *2.8 of [bib/WhiteheadRussell] p. 108.
thm (pm2.8 () () (-> (\/ ps ch) (-> (\/ (-. ch) th) (\/ ps th))) ps th orc (\/ (-. ch) th) a1d ch ps pm2.24 th orim1d jaoi)
(-> (\/ ps ch) (-> (\/ (-. ch) th) (\/ ps th)))
edit