Theorem biimpi

Infer an implication from a logical equivalence. Inference associated with biimp. (Contributed by NM, 29-Dec-1992.)

Hypothesis
biimpi.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
biimpi.1
\( \vdash \varphi \leftrightarrow \psi \)
biimp
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
ax-mp l0 _