Theorem nfvd 1942

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

Syntax hints:   → wi 4  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  cbvaldw  2376  cbvald  2445  cbvaldva  2447  cbvexdva  2448  sbiedv  2542  nfmodv  2593  nfabdw  2952  cbvexeqsetf  3478  nfunid  4879  nfopabd  5180  copsexgwOLD  5471  nfiotadw  6493  iota2d  6522  iota2  6523  riota5f  7393  oprabidw  7439  opiota  8052  mpoxopoveq  8211  nfttrcld  9675  axrepndlem1  10573  axunndlem1  10576  fproddivf  16037  nfchnd  18663  xrofsup  33049  dvelimalcasei  35405  dvelimexcasei  35407  axsepg2  35472  axsepg3  35473  axsepg3ALT  35474  axsepg4  35475  axsepg5  35476  axnulg  35477  axpowg2  35479  axpowg3  35480  bj-cbvaldvav  37323  bj-cbvexdvav  37324  opelopabbv  37670  brabd  37675  cbveud  37901  cbvreud  37902  fvineqsneu  37940  wl-mo2t  38113  wl-sb8eut  38116  wl-sb8eutv  38117  wl-issetft  38120  riotasv2d  39616  cdleme42b  41137  dihvalcqpre  41894  mapdheq  42387  hdmap1eq  42460  hdmapval2lem  42490