Theorem ibir

Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)

Hypothesis
ibir.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
ibir.1
bicomd _
ibi _