Theorem jctr

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

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