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