imdi Show Code edit
## Distributive Property
## right('Distribute', 'L') left('Distribute', '-L')
thm (imdi () () (<-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
ph ps ch ax-2
(-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
ph ps ch pm2.86
(-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
impbii)
(<-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
edit