syl5com Show Code edit
# Hmm, this is the kind of thing where it's easier to just use syl5 com12
# rather than introduce a new name syl5com ... There should be a proof
# complexity metric that reflects that.
## Syllogism & Commute Antecedents
thm (syl5com () (1 (-> ph (-> ps ch)) 2 (-> th ps)) (-> th (-> ph ch))
1 2 syl5 com12)
(-> th (-> ph ch))
edit