Theorem nfvd 1916

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  cbvaldw  2340  cbvald  2409  cbvaldva  2411  cbvexdva  2412  sbiedv  2506  nfmodv  2556  nfabdw  2917  cbvexeqsetf  3452  nfunid  4866  nfopabd  5163  copsexgw  5435  nfiotadw  6448  iota2d  6477  iota2  6478  riota5f  7340  oprabidw  7386  opiota  8000  mpoxopoveq  8158  nfttrcld  9611  axrepndlem1  10494  axunndlem1  10497  fproddivf  15901  nfchnd  18525  xrofsup  32775  dvelimalcasei  35160  dvelimexcasei  35162  axsepg2  35166  axsepg2ALT  35167  axnulg  35191  bj-cbvaldvav  36920  bj-cbvexdvav  36921  opelopabbv  37260  brabd  37265  cbveud  37489  cbvreud  37490  fvineqsneu  37528  wl-mo2t  37692  wl-sb8eut  37695  wl-sb8eutv  37696  wl-issetft  37699  riotasv2d  39129  cdleme42b  40650  dihvalcqpre  41407  mapdheq  41900  hdmap1eq  41973  hdmapval2lem  42003