Theorem anim1i

Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

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