Theorem nfvd 1917

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

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2343  cbvald  2412  cbvaldva  2414  cbvexdva  2415  sbiedv  2509  nfmodv  2560  nfabdw  2921  cbvexeqsetf  3445  nfunid  4857  nfopabd  5154  copsexgw  5436  nfiotadw  6449  iota2d  6478  iota2  6479  riota5f  7343  oprabidw  7389  opiota  8003  mpoxopoveq  8160  nfttrcld  9620  axrepndlem1  10504  axunndlem1  10507  fproddivf  15941  nfchnd  18566  xrofsup  32860  dvelimalcasei  35239  dvelimexcasei  35241  axsepg2  35246  axsepg2ALT  35247  axnulg  35272  bj-cbvaldvav  37123  bj-cbvexdvav  37124  opelopabbv  37470  brabd  37475  cbveud  37699  cbvreud  37700  fvineqsneu  37738  wl-mo2t  37911  wl-sb8eut  37914  wl-sb8eutv  37915  wl-issetft  37918  riotasv2d  39414  cdleme42b  40935  dihvalcqpre  41692  mapdheq  42185  hdmap1eq  42258  hdmapval2lem  42288