Theorem sbrim

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) Avoid ax-10 . (Revised by Gino Giotto, 20-Nov-2024)

	Ref	Expression
Hypothesis	sbrim.1	⊢ Ⅎ 𝑥 𝜑
Assertion	sbrim	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbrim.1	⊢ Ⅎ 𝑥 𝜑
2		bi2.04	⊢ ( ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) )
3	2	albii	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) )
4	1	19.21	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
5	3 4	bitri	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
6	5	imbi2i	⊢ ( ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ( 𝑡 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
7		bi2.04	⊢ ( ( 𝑡 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
8	6 7	bitri	⊢ ( ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
9	8	albii	⊢ ( ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
10		df-sb	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) )
11		df-sb	⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
12	11	imbi2i	⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝜑 → ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
13		19.21v	⊢ ( ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
14	12 13	bitr4i	⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
15	9 10 14	3bitr4i	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )