Theorem biimpd

Deduce an implication from a logical equivalence. Deduction associated with biimp and biimpi. (Contributed by NM, 11-Jan-1993.)

Hypothesis
biimpd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
biimpd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
biimp
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \psi \rightarrow \chi \)
syl l0 _