ancomsd Show Code edit
# Deduction commuting conjunction in antecedent.
## Commute Conjunction
thm (ancomsd () (ancomsd.1 (-> ph (-> (/\ ps ch) th))) (-> ph (-> (/\ ch ps) th)) ancomsd.1 ch ps ancom syl5ib)
(-> ph (-> (/\ ch ps) th))
edit