imdistanri Show Code edit
# Distribution of implication with conjunction.
## Distributive Property
thm (imdistanri () (imdistanri.1 (-> ph (-> ps ch))) (-> (/\ ps ph) (/\ ch ph)) imdistanri.1 com12 impac)
(-> (/\ ps ph) (/\ ch ph))
edit