ancom31s Show Code edit
# Deduction rearranging conjuncts.
## Rearrangement conjunction
thm (ancom31s () (an1rs.1 (-> (/\ (/\ ph ps) ch) th)) (-> (/\ (/\ ch ps) ph) th) an1rs.1 exp31 com13 imp31)
(-> (/\ (/\ ch ps) ph) th)
edit