This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ Ⅎ x φ$
	nfsbd.2	$⊢ φ \to Ⅎ z ψ$
Assertion	nfsbd	$⊢ φ \to Ⅎ z [y/ x] ψ$

Proof

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