Theorem sblbis

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

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