imdistani Show Code edit
# Distribution of implication with conjunction.
## Distributive Property
thm (imdistani () (imdistani.1 (-> ph (-> ps ch))) (-> (/\ ph ps) (/\ ph ch)) imdistani.1 anc2li imp)
(-> (/\ ph ps) (/\ ph ch))
edit