Theorem sbimd

Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise [df-sb]. (Revised by Steven Nguyen, 9-Jul-2023.)

Hypotheses
sbimd.1
\( \vdash \Finv x \, \varphi \)
sbimd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow [ y' / x ] \, \psi \rightarrow [ y' / x ] \, \chi \)
Proof
l0
sbimd.1
sbimd.2
l2
alrimi l0 _
\( \vdash \varphi \rightarrow \forall x \, (\psi \rightarrow \chi) \)
spsbim
\( \vdash \forall x \, (\psi \rightarrow \chi) \rightarrow [ y' / x ] \, \psi \rightarrow [ y' / x ] \, \chi \)
syl l2 _