Theorem impbid21d

Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.)

Hypotheses
impbid21d.1
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
impbid21d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
Proof
l0
impbid21d.1
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
l1
impbid21d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \chi \)
impbi
\( \vdash (\chi \rightarrow \theta) \rightarrow (\theta \rightarrow \chi) \rightarrow (\chi \leftrightarrow \theta) \)
syl2imc l0 l1 _