Theorem nfvd 1947

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

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

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

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  cbvaldw  2367  cbvald  2436  cbvaldva  2438  cbvexdva  2439  sbiedv  2533  nfmodv  2584  nfabdw  2943  cbvexeqsetf  3465  nfunid  4872  nfopabd  5172  copsexgwOLD  5460  nfiotadw  6499  iota2d  6528  iota2  6529  riota5f  7407  oprabidw  7453  opiota  8072  mpoxopoveq  8241  nfttrcld  9716  axrepndlem1  10682  axunndlem1  10685  fproddivf  16161  nfchnd  18792  xrofsup  33407  dvelimalcasei  35754  dvelimexcasei  35756  axsepg2  35866  axsepg3  35867  axsepg3ALT  35868  axsepg4  35869  axsepg5  35870  axnulg  35871  axpowg2  35873  axpowg3  35874  bj-cbvaldvav  37809  bj-cbvexdvav  37810  opelopabbv  38171  brabd  38176  cbveud  38402  cbvreud  38403  fvineqsneu  38441  wl-mo2t  38614  wl-sb8eut  38617  wl-sb8eutv  38618  wl-issetft  38621  findcard4  38739  riotasv2d  40121  cdleme42b  41642  dihvalcqpre  42399  mapdheq  42892  hdmap1eq  42965  hdmapval2lem  42995