Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 23-May-2024. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hbsbwOLD.1	⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
Assertion	hbsbwOLD	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		hbsbwOLD.1	⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
2	1	nf5i	⊢ Ⅎ 𝑧 𝜑
3	2	nfsbv	⊢ Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑
4	3	nf5ri	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )