com24 Show Code edit
## Commute Second and Fourth Antecedents
thm (com24 () (1 (-> ph (-> ps (-> ch (-> th ta)))))
(-> ph (-> th (-> ch (-> ps ta))))
1 com23 com34 com23)
(-> ph (-> th (-> ch (-> ps ta))))
edit