syld Show Code edit
## Syllogism Deduction
##
## Notice that this has the same form as syl with ph added in front of each
## hypothesis and conclusion. When all theorems referenced in a proof are converted in this
## way, we can replace ph with a hypothesis of the proof, allowing the hypothesis to be
## eliminated with id and become an antecedent.
##
thm (syld () (1 (-> ph (-> ps ch)) 2 (-> ph (-> ch th))) (-> ph (-> ps th))
1 2 ps imim2d mpd)
(-> ph (-> ps th))
edit