Theorem jctird

Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses
jctird.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
jctird.2
\( \vdash \varphi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \wedge \theta \)
Proof
l0
jctird.1
jctird.2
a1d _
jcad l0 _