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	|- F/ x ph
	nfsbd.2	|- ( ph -> F/ z ps )
Assertion	nfsbd	|- ( ph -> F/ z [ y / x ] ps )

Proof

Step	Hyp	Ref	Expression
1		nfsbd.1	|- F/ x ph
2		nfsbd.2	|- ( ph -> F/ z ps )
3	1 2	alrimi	|- ( ph -> A. x F/ z ps )
4		nfsb4t	|- ( A. x F/ z ps -> ( -. A. z z = y -> F/ z [ y / x ] ps ) )
5	3 4	syl	|- ( ph -> ( -. A. z z = y -> F/ z [ y / x ] ps ) )
6		axc16nf	|- ( A. z z = y -> F/ z [ y / x ] ps )
7	5 6	pm2.61d2	|- ( ph -> F/ z [ y / x ] ps )