Theorem nfvd 1915

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  cbvaldw  2336  cbvald  2405  cbvaldva  2407  cbvexdva  2408  sbiedv  2502  nfmodv  2552  nfabdw  2913  cbvexeqsetf  3459  nfunid  4873  nfopabd  5170  copsexgw  5445  nfiotadw  6455  iota2d  6487  iota2  6488  riota5f  7354  oprabidw  7400  opiota  8017  mpoxopoveq  8175  nfttrcld  9639  axrepndlem1  10521  axunndlem1  10524  fproddivf  15929  xrofsup  32663  dvelimalcasei  35039  dvelimexcasei  35041  axsepg2  35045  axsepg2ALT  35046  axnulg  35055  bj-cbvaldvav  36764  bj-cbvexdvav  36765  opelopabbv  37104  brabd  37109  cbveud  37333  cbvreud  37334  fvineqsneu  37372  wl-mo2t  37536  wl-sb8eut  37539  wl-sb8eutv  37540  wl-issetft  37543  riotasv2d  38923  cdleme42b  40445  dihvalcqpre  41202  mapdheq  41695  hdmap1eq  41768  hdmapval2lem  41798