Theorem spsbbi
Biconditional property for substitution. Closed form of sbbii.
Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) Revise
[df-sb]. (Revised by BJ, 22-Dec-2020.)
Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow ([ t' / x ] \, \varphi \leftrightarrow [ t' / x ] \, \psi) \)
Proof
biimp
l1
alimi _
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
spsbim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow [ t' / x ] \, \varphi \rightarrow [ t' / x ] \, \psi \)
l3
syl l1 _
biimpr
l5
alimi _
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow \forall x \, (\psi \rightarrow \varphi) \)
spsbim
\( \vdash \forall x \, (\psi \rightarrow \varphi) \rightarrow [ t' / x ] \, \psi \rightarrow [ t' / x ] \, \varphi \)
syl l5 _
impbid l3 _