Theorem bitr3d

Deduction form of bitr3i. (Contributed by NM, 14-May-1993.)

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