Theorem nfvd 1915

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  cbvaldw  2336  cbvald  2405  cbvaldva  2407  cbvexdva  2408  sbiedv  2502  nfmodv  2552  nfabdw  2913  cbvexeqsetf  3462  nfunid  4877  nfopabd  5175  copsexgw  5450  nfiotadw  6467  iota2d  6499  iota2  6500  riota5f  7372  oprabidw  7418  opiota  8038  mpoxopoveq  8198  nfttrcld  9663  axrepndlem1  10545  axunndlem1  10548  fproddivf  15953  xrofsup  32690  dvelimalcasei  35066  dvelimexcasei  35068  axsepg2  35072  axsepg2ALT  35073  axnulg  35082  bj-cbvaldvav  36791  bj-cbvexdvav  36792  opelopabbv  37131  brabd  37136  cbveud  37360  cbvreud  37361  fvineqsneu  37399  wl-mo2t  37563  wl-sb8eut  37566  wl-sb8eutv  37567  wl-issetft  37570  riotasv2d  38950  cdleme42b  40472  dihvalcqpre  41229  mapdheq  41722  hdmap1eq  41795  hdmapval2lem  41825