com14 Show Code edit
## Commute First and Fourth Antecedents
thm (com14 () (1 (-> ph (-> ps (-> ch (-> th ta)))))
(-> th (-> ps (-> ch (-> ph ta))))
1 com3l com34 com3r)
(-> th (-> ps (-> ch (-> ph ta))))
edit