Theorem imbi1i

Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis
imbi1i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \leftrightarrow \psi \rightarrow \chi \)
Proof
l0
imbi1i.1
\( \vdash \varphi \leftrightarrow \psi \)
imbi1
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \chi \leftrightarrow \psi \rightarrow \chi) \)
ax-mp l0 _