pm5.44 Show Code edit
# Theorem *5.44 of [bib/WhiteheadRussell] p. 125.
thm (pm5.44 () () (-> (-> ph ps) (<-> (-> ph ch) (-> ph (/\ ps ch)))) ph ps ch jcab baibr)
(-> (-> ph ps) (<-> (-> ph ch) (-> ph (/\ ps ch))))
edit