Theorem sbied

Conversion of implicit substitution to explicit substitution (deduction version of sbie) Usage of this theorem is discouraged because it depends on [ax-13]. See sbiedw, sbiedvw for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.)

Hypotheses
sbied.1
\( \vdash \Finv x \, \varphi \)
sbied.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
sbied.3
\( \vdash \varphi \rightarrow x = y' \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow ([ y' / x ] \, \psi \leftrightarrow \chi) \)
Proof
sbied.1
l1
sbrim _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow [ y' / x ] \, \psi \)
l2
sbied.1
sbied.2
l4
nfim1 l2 _
sbied.3
com12 _
pm5.74d _
sbie l4 _
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \chi \)
bitr3i l1 _
pm5.74ri _