pm5.15 Show Code edit
# Theorem *5.15 of [bib/WhiteheadRussell] p. 124.
thm (pm5.15 () () (\/ (<-> ph ps) (<-> ph (-. ps))) ph ps pm5.18 biimpri con1i orri)
(\/ (<-> ph ps) (<-> ph (-. ps)))
edit