Theorem anc2ri

Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)

Hypothesis
anc2ri.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \wedge \varphi \)
Proof
l0
anc2ri.1
id
jctird l0 _