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