imdistand Show Code edit
# Distribution of implication with conjunction (deduction rule).
## Distributive Property
thm (imdistand () (imdistand.1 (-> ph (-> ps (-> ch th)))) (-> ph (-> (/\ ps ch) (/\ ps th))) imdistand.1 ps ch th imdistan sylib)
(-> ph (-> (/\ ps ch) (/\ ps th)))
edit