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  2342  cbvald  2411  cbvaldva  2413  cbvexdva  2414  sbiedv  2508  nfmodv  2559  nfabdw  2920  cbvexeqsetf  3444  nfunid  4856  nfopabd  5153  copsexgwOLD  5444  nfiotadw  6457  iota2d  6486  iota2  6487  riota5f  7352  oprabidw  7398  opiota  8012  mpoxopoveq  8169  nfttrcld  9631  axrepndlem1  10515  axunndlem1  10518  fproddivf  15952  nfchnd  18577  xrofsup  32840  dvelimalcasei  35218  dvelimexcasei  35220  axsepg2  35225  axsepg2ALT  35226  axnulg  35251  bj-cbvaldvav  37110  bj-cbvexdvav  37111  opelopabbv  37457  brabd  37462  cbveud  37688  cbvreud  37689  fvineqsneu  37727  wl-mo2t  37900  wl-sb8eut  37903  wl-sb8eutv  37904  wl-issetft  37907  riotasv2d  39403  cdleme42b  40924  dihvalcqpre  41681  mapdheq  42174  hdmap1eq  42247  hdmapval2lem  42277