Theorem 2sbbii

Infer double substitution into both sides of a logical equivalence. (Contributed by AV, 30-Jul-2023.)

Hypothesis
sbbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash [ t' / x ] \, [ u' / y ] \, \varphi \leftrightarrow [ t' / x ] \, [ u' / y ] \, \psi \)
Proof
sbbii.1
sbbii _
sbbii _