jctl Show Code edit
# Inference conjoining a theorem to the left of a consequent.
## Add theorem to the left of a consequent
thm (jctl () (jctl.1 ps) (-> ph (/\ ps ph)) jctl.1 ph a1i ph id jca)
(-> ph (/\ ps ph))
edit