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  3453  nfunid  4867  nfopabd  5163  copsexgw  5437  nfiotadw  6445  iota2d  6474  iota2  6475  riota5f  7338  oprabidw  7384  opiota  8001  mpoxopoveq  8159  nfttrcld  9625  axrepndlem1  10505  axunndlem1  10508  fproddivf  15913  xrofsup  32729  dvelimalcasei  35062  dvelimexcasei  35064  axsepg2  35068  axsepg2ALT  35069  axnulg  35078  bj-cbvaldvav  36796  bj-cbvexdvav  36797  opelopabbv  37136  brabd  37141  cbveud  37365  cbvreud  37366  fvineqsneu  37404  wl-mo2t  37568  wl-sb8eut  37571  wl-sb8eutv  37572  wl-issetft  37575  riotasv2d  38955  cdleme42b  40477  dihvalcqpre  41234  mapdheq  41727  hdmap1eq  41800  hdmapval2lem  41830