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 1785

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 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2343  cbvald  2412  cbvaldva  2414  cbvexdva  2415  sbiedv  2509  nfmodv  2560  nfabdw  2921  cbvexeqsetf  3445  nfunid  4857  nfopabd  5154  copsexgw  5438  nfiotadw  6451  iota2d  6480  iota2  6481  riota5f  7345  oprabidw  7391  opiota  8005  mpoxopoveq  8162  nfttrcld  9622  axrepndlem1  10506  axunndlem1  10509  fproddivf  15943  nfchnd  18568  xrofsup  32855  dvelimalcasei  35234  dvelimexcasei  35236  axsepg2  35241  axsepg2ALT  35242  axnulg  35267  bj-cbvaldvav  37126  bj-cbvexdvav  37127  opelopabbv  37473  brabd  37478  cbveud  37702  cbvreud  37703  fvineqsneu  37741  wl-mo2t  37914  wl-sb8eut  37917  wl-sb8eutv  37918  wl-issetft  37921  riotasv2d  39417  cdleme42b  40938  dihvalcqpre  41695  mapdheq  42188  hdmap1eq  42261  hdmapval2lem  42291