ancomd Show Code edit
# Commutation of conjuncts in consequent. (Contributed by Jeff Hankins,
# 14-Aug-2009.)
## Commute Conjunction
thm (ancomd () (ancomd.1 (-> ph (/\ ps ch))) (-> ph (/\ ch ps)) ancomd.1 ps ch ancom sylib)
(-> ph (/\ ch ps))
edit