Theorem sbrimv

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim not depending on ax-10 , but with disjoint variables. (Contributed by Wolf Lammen, 28-Jan-2024)

	Ref	Expression
Hypothesis	sbrim.1	$$⊢Ⅎx\phi$$
Assertion	sbrimv	$$⊢\left[y/x\right]\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \left[y/x\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbrim.1	$$⊢Ⅎx\phi$$
2	1	19.21	$$⊢\forall x\left(\phi \to \left(x=y\to \psi \right)\right)\leftrightarrow \left(\phi \to \forall x\left(x=y\to \psi \right)\right)$$
3	2	sbrimvlem	$$⊢\left[y/x\right]\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \left[y/x\right]\psi \right)$$