Theorem simp1bi

Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis
3simp1bi.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \wedge \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
3simp1bi.1
biimpi _
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
simp1d _