Theorem sbbidv

Deduction substituting both sides of a biconditional, with \( \varphi \) and \( x \) disjoint. See also sbbid. (Contributed by Wolf Lammen, 6-May-2023.) (Proof shortened by Steven Nguyen, 6-Jul-2023.)

Hypothesis
sbbidv.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ t' / x ] \, \psi \leftrightarrow [ t' / x ] \, \chi) \)
Proof
sbbidv.1
l1
alrimiv _
\( \vdash \varphi \rightarrow \forall x \, (\psi \leftrightarrow \chi) \)
spsbbi
\( \vdash \forall x \, (\psi \leftrightarrow \chi) \rightarrow ([ t' / x ] \, \psi \leftrightarrow [ t' / x ] \, \chi) \)
syl l1 _