Theorem nfvd 1950

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

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

This theorem is used by:  cbvaldw  2371  cbvald  2439  cbvaldva  2441  cbvexdva  2442  sbiedv  2536  nfmodv  2587  nfabdw  2947  cbvexeqsetf  3469  nfunid  4878  nfopabd  5179  copsexgwOLD  5468  nfiotadw  6523  iota2d  6553  iota2  6554  riota5f  7436  oprabidw  7482  opiota  8105  mpoxopoveq  8274  nfttrcld  9748  axrepndlem1  10716  axunndlem1  10719  fproddivf  16198  nfchnd  18835  xrofsup  33455  dvelimalcasei  35817  dvelimexcasei  35819  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg4  35952  axsepg5  35953  axnulg  35954  axpowg2  35956  axpowg3  35957  bj-cbvaldvav  37930  bj-cbvexdvav  37931  opelopabbv  38335  brabd  38337  cbveud  38563  cbvreud  38564  fvineqsneu  38602  wl-mo2t  38775  wl-sb8eut  38778  wl-sb8eutv  38779  wl-issetft  38782  findcard4  38900  riotasv2d  40280  cdleme42b  41801  dihvalcqpre  42558  mapdheq  43051  hdmap1eq  43124  hdmapval2lem  43154