Theorem simplbi2com

A deduction eliminating a conjunct, similar to simplbi2. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)

Hypothesis
simplbi2com.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \chi \rightarrow \psi \rightarrow \varphi \)
Proof
simplbi2com.1
simplbi2 _
com12 _