Theorem biimprd

Deduce a converse implication from a logical equivalence. Deduction associated with biimpr and biimpri. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis
biimprd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
Proof
l0
id
\( \vdash \chi \rightarrow \chi \)
biimprd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
imbitrrid l0 _