pm5.501 Show Code edit
# Theorem *5.501 of [bib/WhiteheadRussell] p. 125.
thm (pm5.501 () () (-> ph (<-> ps (<-> ph ps))) ph ps ibib pm5.74ri)
(-> ph (<-> ps (<-> ph ps)))
edit