Theorem bitr2d

Deduction form of bitr2i. (Contributed by NM, 9-Jun-2004.)

Hypotheses
bitr2d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bitr2d.2
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi) \)
Proof
l0
bitr2d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bitr2d.2
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \theta) \)
bitrd l0 _
bicomd _