com13 Show Code edit
## Commute First and Third Antecedents
thm (com13 () (1 (-> ph (-> ps (-> ch th)))) (-> ch (-> ps (-> ph th)))
1 com23 com12 com23)
(-> ch (-> ps (-> ph th)))
edit