pm2.26 Show Code edit
# Theorem *2.26 of [bib/WhiteheadRussell] p. 104.
thm (pm2.26 () () (\/ (-. ph) (-> (-> ph ps) ps)) ph notnot2 ps imim1i com12 orri)
(\/ (-. ph) (-> (-> ph ps) ps))
edit