pm2.41 Show Code edit
# Theorem *2.41 of [bib/WhiteheadRussell] p. 106.
## Remove Repeated Disjunct
thm (pm2.41 () () (-> (\/ ps (\/ ph ps)) (\/ ph ps)) ps ph olc (\/ ph ps) id jaoi)
(-> (\/ ps (\/ ph ps)) (\/ ph ps))
edit