Theorem nfsbd

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

	Ref	Expression
Hypotheses	nfsbd.1	$$⊢Ⅎx\phi$$
	nfsbd.2	$$⊢\phi \to Ⅎz\psi$$
Assertion	nfsbd	$$⊢\phi \to Ⅎz\left[y/x\right]\psi$$

Proof

Step	Hyp	Ref	Expression
1		nfsbd.1	$$⊢Ⅎx\phi$$
2		nfsbd.2	$$⊢\phi \to Ⅎz\psi$$
3	1 2	alrimi	$$⊢\phi \to \forall xℲz\psi$$
4		nfsb4t	$$⊢\forall xℲz\psi \to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\psi \right)$$
5	3 4	syl	$$⊢\phi \to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\psi \right)$$
6		axc16nf	$$⊢\forall zz=y\to Ⅎz\left[y/x\right]\psi$$
7	5 6	pm2.61d2	$$⊢\phi \to Ⅎz\left[y/x\right]\psi$$