jctir Show Code edit
## Add theorem to the right of a consequent
thm (jctir () (jctir.1 (-> ph ps) jctir.2 ch) (-> ph (/\ ps ch)) jctir.1 jctir.2 ph a1i jca)
(-> ph (/\ ps ch))
edit