com34 Show Code edit
## Commute Third and Fourth Antecedents
thm (com34 () (1 (-> ph (-> ps (-> ch (-> th ta)))))
(-> ph (-> ps (-> th (-> ch ta))))
1 ch th ta pm2.04 syl6)
(-> ph (-> ps (-> th (-> ch ta))))
edit