Theorem imbi1d

Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis
imbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \theta \leftrightarrow \chi \rightarrow \theta) \)
Proof
imbid.1
biimprd _
l2
imim1d _
imbid.1
biimpd _
imim1d _
impbid l2 _