Theorem sbrimvwOLD
Obsolete version of sbrimvw as of 5-Jun-2026. (Contributed by Wolf
Lammen, 29-Jan-2024.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
Proof
l0
sb6
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \)
bi2.04
l2
albii _
\( \vdash \forall x \, (\varphi \rightarrow x = y' \rightarrow \psi) \leftrightarrow \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \)
19.21v
\( \vdash \forall x \, (\varphi \rightarrow x = y' \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \psi) \)
l4
3bitr2i l0 l2 _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \psi) \)
sb6
imbi2i _
\( \vdash \varphi \rightarrow [ y' / x ] \, \psi \leftrightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \psi) \)
bitr4i l4 _