Theorem jctir

Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses
jctil.1
\( \vdash \varphi \rightarrow \psi \)
jctil.2
\( \vdash \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
Proof
l0
jctil.1
jctil.2
a1i _
jca l0 _