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  2340  cbvald  2412  cbvaldva  2414  cbvexdva  2415  sbiedv  2509  nfmodv  2559  nfabdw  2927  cbvexeqsetf  3495  nfunid  4913  nfopabd  5211  copsexgw  5495  nfiotadw  6517  iota2d  6549  iota2  6550  riota5f  7416  oprabidw  7462  opiota  8084  mpoxopoveq  8244  nfttrcld  9750  axrepndlem1  10632  axunndlem1  10635  fproddivf  16023  xrofsup  32771  dvelimalcasei  35090  dvelimexcasei  35092  axsepg2  35096  axsepg2ALT  35097  axnulg  35106  bj-cbvaldvav  36804  bj-cbvexdvav  36805  opelopabbv  37144  brabd  37149  cbveud  37373  cbvreud  37374  fvineqsneu  37412  wl-mo2t  37576  wl-sb8eut  37579  wl-sb8eutv  37580  wl-issetft  37583  riotasv2d  38958  cdleme42b  40480  dihvalcqpre  41237  mapdheq  41730  hdmap1eq  41803  hdmapval2lem  41833