Theorem nfsbd

Description: Deduction version of nfsb . (Contributed by NM, 15-Feb-2013) Usage of this theorem is discouraged because it depends on ax-13 . Use nfsbv instead. (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfsbd.1	⊢ Ⅎ 𝑥 𝜑
	nfsbd.2	⊢ ( 𝜑 → Ⅎ 𝑧 𝜓 )
Assertion	nfsbd	⊢ ( 𝜑 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfsbd.1	⊢ Ⅎ 𝑥 𝜑
2		nfsbd.2	⊢ ( 𝜑 → Ⅎ 𝑧 𝜓 )
3	1 2	alrimi	⊢ ( 𝜑 → ∀ 𝑥 Ⅎ 𝑧 𝜓 )
4		nfsb4t	⊢ ( ∀ 𝑥 Ⅎ 𝑧 𝜓 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜓 ) )
5	3 4	syl	⊢ ( 𝜑 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜓 ) )
6		axc16nf	⊢ ( ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜓 )
7	5 6	pm2.61d2	⊢ ( 𝜑 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜓 )