Theorem sbrbis

Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)

Hypothesis
sbrbis.1
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \chi) \leftrightarrow (\psi \leftrightarrow [ y' / x ] \, \chi) \)
Proof
l0
sbbi
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \chi) \leftrightarrow ([ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \chi) \)
sbrbis.1
bibi1i _
\( \vdash [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \chi \leftrightarrow (\psi \leftrightarrow [ y' / x ] \, \chi) \)
bitri l0 _