anassrs Show Code edit
# Associative law for conjunction applied to antecedent (eliminates
# syllogism).
## Associative Property
thm (anassrs () (anassrs.1 (-> (/\ ph (/\ ps ch)) th)) (-> (/\ (/\ ph ps) ch) th) anassrs.1 exp32 imp31)
(-> (/\ (/\ ph ps) ch) th)
edit