Theorem jctl

Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)

Hypothesis
jctl.1
\( \vdash \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \varphi \)
Proof
l0
id
jctl.1
jctil l0 _