Theorem 3bitr4g

More general version of 3bitr4i. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)

Hypotheses
3bitr4g.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3bitr4g.2
\( \vdash \theta \leftrightarrow \psi \)
3bitr4g.3
\( \vdash \tau \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Proof
l0
3bitr4g.2
\( \vdash \theta \leftrightarrow \psi \)
3bitr4g.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l2
bitrid l0 _
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \chi) \)
3bitr4g.3
\( \vdash \tau \leftrightarrow \chi \)
bitr4di l2 _