Theorem jccir

Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also [ex-natded5.3i]. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.)

Hypotheses
jccir.1
\( \vdash \varphi \rightarrow \psi \)
jccir.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
Proof
l0
jccir.1
l1
jccir.1
\( \vdash \varphi \rightarrow \psi \)
jccir.2
\( \vdash \psi \rightarrow \chi \)
syl l1 _
jca l0 _