pm5.41 Show Code edit
## Distributive Property
thm (pm5.41 () () (<-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
ph ps ch imdi bicomi)
(<-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
edit