Theorem nfvd 1918

Description: nfv 1917 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1897. (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 1917	. 2 ⊢ Ⅎ𝑥𝜓
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2334  cbvald  2406  cbvaldva  2408  cbvexdva  2409  sbiedv  2503  nfmodv  2553  nfabdw  2926  vtoclgft  3540  vtocldOLD  3543  sbciedOLD  3823  nfunid  4914  nfopabd  5216  copsexgw  5490  nfiotadw  6498  iota2d  6531  iota2  6532  riota5f  7393  oprabidw  7439  opiota  8044  mpoxopoveq  8203  nfttrcld  9704  axrepndlem1  10586  axunndlem1  10589  fproddivf  15930  xrofsup  31975  bj-cbvaldvav  35676  bj-cbvexdvav  35677  opelopabbv  36019  brabd  36024  cbveud  36248  cbvreud  36249  fvineqsneu  36287  wl-mo2t  36435  wl-sb8eut  36437  wl-issetft  36439  riotasv2d  37822  cdleme42b  39344  dihvalcqpre  40101  mapdheq  40594  hdmap1eq  40667  hdmapval2lem  40697