Theorem nfvd 1922

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

Syntax hints:   → wi 4  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  cbvaldw  2346  cbvald  2415  cbvaldva  2417  cbvexdva  2418  sbiedv  2512  nfmodv  2563  nfabdw  2922  cbvexeqsetf  3446  nfunid  4844  nfopabd  5140  copsexgwOLD  5431  nfiotadw  6444  iota2d  6473  iota2  6474  riota5f  7341  oprabidw  7387  opiota  8001  mpoxopoveq  8159  nfttrcld  9622  axrepndlem1  10506  axunndlem1  10509  fproddivf  15943  nfchnd  18568  xrofsup  32859  dvelimalcasei  35258  dvelimexcasei  35260  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg4  35324  axsepg5  35325  axnulg  35326  axpowg2  35328  axpowg3  35329  bj-cbvaldvav  37156  bj-cbvexdvav  37157  opelopabbv  37503  brabd  37508  cbveud  37734  cbvreud  37735  fvineqsneu  37773  wl-mo2t  37946  wl-sb8eut  37949  wl-sb8eutv  37950  wl-issetft  37953  riotasv2d  39449  cdleme42b  40970  dihvalcqpre  41727  mapdheq  42220  hdmap1eq  42293  hdmapval2lem  42323