imdistan Show Code edit
# Distribution of implication with conjunction.
## Distributive Property
thm (imdistan () () (<-> (-> ph (-> ps ch)) (-> (/\ ph ps) (/\ ph ch))) ph ps ch anc2l imp3a ph ch pm3.27 (/\ ph ps) imim2i exp3a impbii)
(<-> (-> ph (-> ps ch)) (-> (/\ ph ps) (/\ ph ch)))
edit