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