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  2406  cbvaldva  2408  cbvexdva  2409  sbiedv  2503  nfmodv  2553  nfabdw  2914  cbvexeqsetf  3465  nfunid  4880  nfopabd  5178  copsexgw  5453  nfiotadw  6470  iota2d  6502  iota2  6503  riota5f  7375  oprabidw  7421  opiota  8041  mpoxopoveq  8201  nfttrcld  9670  axrepndlem1  10552  axunndlem1  10555  fproddivf  15960  xrofsup  32697  dvelimalcasei  35073  dvelimexcasei  35075  axsepg2  35079  axsepg2ALT  35080  axnulg  35089  bj-cbvaldvav  36798  bj-cbvexdvav  36799  opelopabbv  37138  brabd  37143  cbveud  37367  cbvreud  37368  fvineqsneu  37406  wl-mo2t  37570  wl-sb8eut  37573  wl-sb8eutv  37574  wl-issetft  37577  riotasv2d  38957  cdleme42b  40479  dihvalcqpre  41236  mapdheq  41729  hdmap1eq  41802  hdmapval2lem  41832