com3l Show Code edit
## Commute Antecedents (Rotate Left)
thm (com3l () (1 (-> ph (-> ps (-> ch th)))) (-> ps (-> ch (-> ph th)))
1 com12 com23)
(-> ps (-> ch (-> ph th)))
edit