an4s Show Code edit
## Rearrange Conjunction
thm (an4s () (an4s.1 (-> (/\ (/\ ph ps) (/\ ch th)) ta)) (-> (/\ (/\ ph ch) (/\ ps th)) ta) ph ch ps th an4 an4s.1 sylbi)
(-> (/\ (/\ ph ch) (/\ ps th)) ta)
edit