Theorem sbiedvw

Conversion of implicit substitution to explicit substitution (deduction version of sbievw ). Version of sbied and sbiedv with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by GG, 29-Jan-2024.)

Hypothesis
sbiedvw.1
\( \vdash \varphi \wedge x = y' \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / x ] \, \psi \leftrightarrow \chi) \)
Proof
l0
sbrimvw
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
sbiedvw.1
expcom _
pm5.74d _
sbievw _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \chi \)
bitr3i l0 _
pm5.74ri _