Theorem nfvd 1945

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

Syntax hints:   → wi 4  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  cbvaldw  2370  cbvald  2439  cbvaldva  2441  cbvexdva  2442  sbiedv  2536  nfmodv  2587  nfabdw  2946  cbvexeqsetf  3470  nfunid  4878  nfopabd  5179  copsexgwOLD  5473  nfiotadw  6495  iota2d  6524  iota2  6525  riota5f  7395  oprabidw  7441  opiota  8052  mpoxopoveq  8211  nfttrcld  9675  axrepndlem1  10572  axunndlem1  10575  fproddivf  16037  nfchnd  18662  xrofsup  33112  dvelimalcasei  35464  dvelimexcasei  35466  axsepg2  35553  axsepg3  35554  axsepg3ALT  35555  axsepg4  35556  axsepg5  35557  axnulg  35558  axpowg2  35560  axpowg3  35561  bj-cbvaldvav  37438  bj-cbvexdvav  37439  opelopabbv  37787  brabd  37792  cbveud  38018  cbvreud  38019  fvineqsneu  38057  wl-mo2t  38230  wl-sb8eut  38233  wl-sb8eutv  38234  wl-issetft  38237  riotasv2d  39731  cdleme42b  41252  dihvalcqpre  42009  mapdheq  42502  hdmap1eq  42575  hdmapval2lem  42605