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