pm5.35 Show Code edit
# Theorem *5.35 of [bib/WhiteheadRussell] p. 125.
thm (pm5.35 () () (-> (/\ (-> ph ps) (-> ph ch)) (-> ph (<-> ps ch))) (-> ph ps) (-> ph ch) pm5.1 pm5.74rd)
(-> (/\ (-> ph ps) (-> ph ch)) (-> ph (<-> ps ch)))
edit