Theorem sbrimvw

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim based on fewer axioms, but with more disjoint variable conditions. (Contributed by Wolf Lammen, 29-Jan-2024) Remove DV condition. (Revised by Wolf Lammen, 5-Jun-2026)

	Ref	Expression
Assertion	sbrimvw	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbv	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
2		sbi1	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
3	1 2	biimtrrid	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
4		sbv	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜑 )
5		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
6	5	sbimi	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
7	4 6	sylbir	⊢ ( ¬ 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
8		ax-1	⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
9	8	sbimi	⊢ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
10	7 9	ja	⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
11	3 10	impbii	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )