Theorem imbi2

Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \rightarrow \varphi \leftrightarrow \chi \rightarrow \psi) \)
Proof
id
imbi2d _