Theorem nfvd 1948

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  cbvaldw  2372  cbvald  2441  cbvaldva  2443  cbvexdva  2444  sbiedv  2538  nfmodv  2589  nfabdw  2948  cbvexeqsetf  3472  nfunid  4880  nfopabd  5181  copsexgwOLD  5475  nfiotadw  6499  iota2d  6528  iota2  6529  riota5f  7401  oprabidw  7447  opiota  8058  mpoxopoveq  8217  nfttrcld  9682  axrepndlem1  10588  axunndlem1  10591  fproddivf  16060  nfchnd  18685  xrofsup  33158  dvelimalcasei  35505  dvelimexcasei  35507  axsepg2  35586  axsepg3  35587  axsepg3ALT  35588  axsepg4  35589  axsepg5  35590  axnulg  35591  axpowg2  35593  axpowg3  35594  bj-cbvaldvav  37471  bj-cbvexdvav  37472  opelopabbv  37820  brabd  37825  cbveud  38051  cbvreud  38052  fvineqsneu  38090  wl-mo2t  38263  wl-sb8eut  38266  wl-sb8eutv  38267  wl-issetft  38270  riotasv2d  39764  cdleme42b  41285  dihvalcqpre  42042  mapdheq  42535  hdmap1eq  42608  hdmapval2lem  42638