anandirs Show Code edit
# Inference that undistributes conjunction in the antecedent.
## Distributive Property
thm (anandirs () (anandirs.1 (-> (/\ (/\ ph ch) (/\ ps ch)) ta)) (-> (/\ (/\ ph ps) ch) ta) anandirs.1 an4s anabsan2)
(-> (/\ (/\ ph ps) ch) ta)
edit