pm5.53 Show Code edit
# Theorem *5.53 of [bib/WhiteheadRussell] p. 125.
thm (pm5.53 () () (<-> (-> (\/ (\/ ph ps) ch) th) (/\ (/\ (-> ph th) (-> ps th)) (-> ch th))) (\/ ph ps) ch th jaob ph ps th jaob (-> ch th) anbi1i bitri)
(<-> (-> (\/ (\/ ph ps) ch) th) (/\ (/\ (-> ph th) (-> ps th)) (-> ch th)))
edit