Theorem bitrd

Deduction form of bitri. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses
bitrd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bitrd.2
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta) \)
Proof
bitrd.1
l1
pm5.74i _
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi \)
bitrd.2
pm5.74i _
\( \vdash \varphi \rightarrow \chi \leftrightarrow \varphi \rightarrow \theta \)
bitri l1 _
pm5.74ri _