Theorem nfvd 1917

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

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2343  cbvald  2412  cbvaldva  2414  cbvexdva  2415  sbiedv  2509  nfmodv  2560  nfabdw  2921  cbvexeqsetf  3457  nfunid  4871  nfopabd  5168  copsexgw  5446  nfiotadw  6459  iota2d  6488  iota2  6489  riota5f  7353  oprabidw  7399  opiota  8013  mpoxopoveq  8171  nfttrcld  9631  axrepndlem1  10515  axunndlem1  10518  fproddivf  15922  nfchnd  18546  xrofsup  32858  dvelimalcasei  35252  dvelimexcasei  35254  axsepg2  35259  axsepg2ALT  35260  axnulg  35285  bj-cbvaldvav  37051  bj-cbvexdvav  37052  opelopabbv  37398  brabd  37403  cbveud  37627  cbvreud  37628  fvineqsneu  37666  wl-mo2t  37830  wl-sb8eut  37833  wl-sb8eutv  37834  wl-issetft  37837  riotasv2d  39333  cdleme42b  40854  dihvalcqpre  41611  mapdheq  42104  hdmap1eq  42177  hdmapval2lem  42207