Theorem sbbi
Equivalence inside and outside of a substitution are equivalent.
(Contributed by NM, 14-May-1993.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \psi) \leftrightarrow ([ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \psi) \)
Proof
dfbi2
l1
sbbii _
\( \vdash [ y' / x ] \, (\varphi \leftrightarrow \psi) \leftrightarrow [ y' / x ] \, ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \)
l2
sbim
sbim
l4
anbi12i l2 _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \wedge [ y' / x ] \, (\psi \rightarrow \varphi) \leftrightarrow ([ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi) \wedge ([ y' / x ] \, \psi \rightarrow [ y' / x ] \, \varphi) \)
l5
sban
\( \vdash [ y' / x ] \, ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \leftrightarrow [ y' / x ] \, (\varphi \rightarrow \psi) \wedge [ y' / x ] \, (\psi \rightarrow \varphi) \)
dfbi2
\( \vdash [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \psi \leftrightarrow ([ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi) \wedge ([ y' / x ] \, \psi \rightarrow [ y' / x ] \, \varphi) \)
3bitr4i l4 l5 _
\( \vdash [ y' / x ] \, ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \leftrightarrow ([ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, \psi) \)
bitri l1 _