Theorem sbrbif

Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypotheses
sbrbif.1
\( \vdash \Finv x \, \chi \)
sbrbif.2
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \chi) \leftrightarrow (\psi \leftrightarrow \chi) \)
Proof
sbrbif.2
l1
sbrbis _
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \chi) \leftrightarrow (\psi \leftrightarrow [ y' / x ] \, \chi) \)
sbrbif.1
sbf _
bibi2i _
\( \vdash \psi \leftrightarrow [ y' / x ] \, \chi \leftrightarrow (\psi \leftrightarrow \chi) \)
bitri l1 _