Theorem ibi

Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)

Hypothesis
ibi.1
\( \vdash \varphi \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
ibi.1
\( \vdash \varphi \rightarrow (\varphi \leftrightarrow \psi) \)
mpbid l0 _