Theorem biimprcd

Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypothesis
biimpcd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \chi \rightarrow \varphi \rightarrow \psi \)
Proof
l0
id
\( \vdash \chi \rightarrow \chi \)
biimpcd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
syl5ibrcom l0 _