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

Metamath Proof Explorer

Theorem nfvd

Description: nfv with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd . (Contributed by Mario Carneiro, 6-Oct-2016)

		Ref	Expression
	Assertion	nfvd	\|- ( ph -> F/ x ps )

Proof

Step	Hyp	Ref	Expression
1		nfv	\|- F/ x ps
2	1	a1i	\|- ( ph -> F/ x ps )