Theorem nfvd 1916

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  cbvaldw  2338  cbvald  2407  cbvaldva  2409  cbvexdva  2410  sbiedv  2504  nfmodv  2554  nfabdw  2916  cbvexeqsetf  3451  nfunid  4860  nfopabd  5154  copsexgw  5425  nfiotadw  6435  iota2d  6464  iota2  6465  riota5f  7326  oprabidw  7372  opiota  7986  mpoxopoveq  8144  nfttrcld  9595  axrepndlem1  10478  axunndlem1  10481  fproddivf  15889  nfchnd  18512  xrofsup  32742  dvelimalcasei  35080  dvelimexcasei  35082  axsepg2  35086  axsepg2ALT  35087  axnulg  35111  bj-cbvaldvav  36837  bj-cbvexdvav  36838  opelopabbv  37177  brabd  37182  cbveud  37406  cbvreud  37407  fvineqsneu  37445  wl-mo2t  37609  wl-sb8eut  37612  wl-sb8eutv  37613  wl-issetft  37616  riotasv2d  38996  cdleme42b  40517  dihvalcqpre  41274  mapdheq  41767  hdmap1eq  41840  hdmapval2lem  41870