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