Theorem 3bitr3g

More general version of 3bitr3i. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)

Hypotheses
3bitr3g.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3bitr3g.2
\( \vdash \psi \leftrightarrow \theta \)
3bitr3g.3
\( \vdash \chi \leftrightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Proof
l0
3bitr3g.2
\( \vdash \psi \leftrightarrow \theta \)
3bitr3g.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l2
bitr3id l0 _
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \chi) \)
3bitr3g.3
\( \vdash \chi \leftrightarrow \tau \)
bitrdi l2 _