Theorem bitr4d

Deduction form of bitr4i. (Contributed by NM, 30-Jun-1993.)

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