Theorem sbbii

Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)

Hypothesis
sbbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow [ t' / x ] \, \psi \)
Proof
sbbii.1
biimpi _
l2
sbimi _
sbbii.1
biimpri _
sbimi _
impbii l2 _