Theorem ancri

Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)

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