Theorem simp2i

Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis
3simp1i.1
\( \vdash \varphi \wedge \psi \wedge \chi \)
Conclusion
\( \vdash \psi \)
Proof
l0
3simp1i.1
\( \vdash \varphi \wedge \psi \wedge \chi \)
simp2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \psi \)
ax-mp l0 _