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  2339  cbvald  2411  cbvaldva  2413  cbvexdva  2414  sbiedv  2508  nfmodv  2558  nfabdw  2920  cbvexeqsetf  3474  nfunid  4889  nfopabd  5187  copsexgw  5465  nfiotadw  6487  iota2d  6519  iota2  6520  riota5f  7390  oprabidw  7436  opiota  8058  mpoxopoveq  8218  nfttrcld  9724  axrepndlem1  10606  axunndlem1  10609  fproddivf  16003  xrofsup  32744  dvelimalcasei  35107  dvelimexcasei  35109  axsepg2  35113  axsepg2ALT  35114  axnulg  35123  bj-cbvaldvav  36821  bj-cbvexdvav  36822  opelopabbv  37161  brabd  37166  cbveud  37390  cbvreud  37391  fvineqsneu  37429  wl-mo2t  37593  wl-sb8eut  37596  wl-sb8eutv  37597  wl-issetft  37600  riotasv2d  38975  cdleme42b  40497  dihvalcqpre  41254  mapdheq  41747  hdmap1eq  41820  hdmapval2lem  41850