Theorem nfvd 1916

Description: nfv 1915 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1895. (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 1915	. 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 1911

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

This theorem is referenced by:  cbvaldw  2342  cbvald  2411  cbvaldva  2413  cbvexdva  2414  sbiedv  2508  nfmodv  2559  nfabdw  2920  cbvexeqsetf  3455  nfunid  4869  nfopabd  5166  copsexgw  5438  nfiotadw  6451  iota2d  6480  iota2  6481  riota5f  7343  oprabidw  7389  opiota  8003  mpoxopoveq  8161  nfttrcld  9619  axrepndlem1  10503  axunndlem1  10506  fproddivf  15910  nfchnd  18534  xrofsup  32847  dvelimalcasei  35232  dvelimexcasei  35234  axsepg2  35238  axsepg2ALT  35239  axnulg  35264  bj-cbvaldvav  37004  bj-cbvexdvav  37005  opelopabbv  37348  brabd  37353  cbveud  37577  cbvreud  37578  fvineqsneu  37616  wl-mo2t  37780  wl-sb8eut  37783  wl-sb8eutv  37784  wl-issetft  37787  riotasv2d  39217  cdleme42b  40738  dihvalcqpre  41495  mapdheq  41988  hdmap1eq  42061  hdmapval2lem  42091