Theorem sbi1

Description: Distribute substitution over implication. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023) Definition df-sb changed. (Revised by Wolf Lammen, 5-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		sbi1lem	⊢ ( ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ∀ 𝑢 ( 𝑢 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝜓 ) ) )
2		sbi1lem	⊢ ( ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ∀ 𝑧 ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜓 ) ) )
3		df-sb	⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ ( ∀ 𝑢 ( 𝑢 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝜓 ) ) ∧ ∀ 𝑧 ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜓 ) ) ) )
4	1 2 3	sylanbrc	⊢ ( ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜓 )
5	4	ex	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )