Theorem imbi2d

Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis
imbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \rightarrow \psi \leftrightarrow \theta \rightarrow \chi) \)
Proof
imbid.1
a1d _
pm5.74d _