Theorem 3anim1i

Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)

Hypothesis
3animi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \psi \wedge \chi \wedge \theta \)
Proof
l0
3animi.1
l1
id
id
3anim123i l0 l1 _