Theorem sbbid

Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on [ax-10] and [ax-13]. (Revised by Wolf Lammen, 24-Nov-2022.) Revise [df-sb]. (Revised by Steven Nguyen, 11-Jul-2023.)

Hypotheses
sbbid.1
\( \vdash \Finv x \, \varphi \)
sbbid.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / x ] \, \psi \leftrightarrow [ y' / x ] \, \chi) \)
Proof
l0
sbbid.1
sbbid.2
l2
alrimi l0 _
\( \vdash \varphi \rightarrow \forall x \, (\psi \leftrightarrow \chi) \)
spsbbi
\( \vdash \forall x \, (\psi \leftrightarrow \chi) \rightarrow ([ y' / x ] \, \psi \leftrightarrow [ y' / x ] \, \chi) \)
syl l2 _