Theorem simp1i

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

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