Theorem nfvd 1917

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

Assertion

Ref	Expression
nfvd	⊢ (𝜑 → Ⅎ𝑥𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfvd

Step	Hyp	Ref	Expression
1		nfv 1916	. 2 ⊢ Ⅎ𝑥𝜓
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-ex 1781  df-nf 1785

This theorem is referenced by:  cbvaldw  2334  cbvald  2406  cbvaldva  2408  cbvexdva  2409  sbiedv  2507  nfmodv  2558  nfabdw  2928  vtoclgft  3501  vtocldOLD  3504  sbciedOLD  3772  nfunid  4856  nfopabd  5155  copsexgw  5423  nfiotadw  6421  iota2d  6454  iota2  6455  riota5f  7303  oprabidw  7348  opiota  7946  mpoxopoveq  8084  nfttrcld  9546  axrepndlem1  10428  axunndlem1  10431  fproddivf  15776  xrofsup  31225  bj-cbvaldvav  35059  bj-cbvexdvav  35060  opelopabbv  35386  brabd  35391  cbveud  35615  cbvreud  35616  fvineqsneu  35654  wl-mo2t  35802  wl-sb8eut  35804  riotasv2d  37191  cdleme42b  38713  dihvalcqpre  39470  mapdheq  39963  hdmap1eq  40036  hdmapval2lem  40066