Theorem 2sbbid

Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.)

Hypotheses
sbbid.1
\( \vdash \Finv x \, \varphi \)
sbbid.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
2sbbid.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \varphi \rightarrow ([ t' / x ] \, [ u' / y ] \, \psi \leftrightarrow [ t' / x ] \, [ u' / y ] \, \chi) \)
Proof
l0
sbbid.1
l1
2sbbid.1
sbbid.2
sbbid l1 _
sbbid l0 _