Theorem ibd

Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi. (Contributed by NM, 26-Jun-2004.)

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