Theorem
anim2i
Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
Hypothesis
anim1i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \wedge \varphi \rightarrow \chi \wedge \psi \)
Proof
l0
id
anim1i.1
anim12i
l0
_
This is the content in the right pane.