Theorem biimpcd

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

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