Theorem simplbiim

Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)

Hypotheses
simplbiim.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
simplbiim.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
simplbiim.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
l1
simprbi _
\( \vdash \varphi \rightarrow \chi \)
simplbiim.2
\( \vdash \chi \rightarrow \theta \)
syl l1 _