Theorem biimpri

Infer a converse implication from a logical equivalence. Inference associated with biimpr. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis
biimpri.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \psi \rightarrow \varphi \)
Proof
biimpri.1
bicomi _
biimpi _