Theorem sbimdv

Deduction substituting both sides of an implication, with \( \varphi \) and \( x \) disjoint. See also sbimd. (Contributed by Wolf Lammen, 6-May-2023.) Revise [df-sb]. (Revised by Steven Nguyen, 6-Jul-2023.)

Hypothesis
sbimdv.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow [ t' / x ] \, \psi \rightarrow [ t' / x ] \, \chi \)
Proof
sbimdv.1
l1
alrimiv _
\( \vdash \varphi \rightarrow \forall x \, (\psi \rightarrow \chi) \)
spsbim
\( \vdash \forall x \, (\psi \rightarrow \chi) \rightarrow [ t' / x ] \, \psi \rightarrow [ t' / x ] \, \chi \)
syl l1 _