jcai Show Code edit
## Replace implication with conjunction
thm (jcai () (jcai.1 (-> ph ps) jcai.2 (-> ph (-> ps ch))) (-> ph (/\ ps ch)) jcai.1 jcai.1 jcai.2 mpd jca)
(-> ph (/\ ps ch))
edit