Theorem nfvd 1934

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

Syntax hints:   → wi 4  Ⅎwnf 1802

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

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803

This theorem is referenced by:  cbvaldw  2368  cbvald  2437  cbvaldva  2439  cbvexdva  2440  sbiedv  2534  nfmodv  2585  nfabdw  2944  cbvexeqsetf  3468  nfunid  4868  nfopabd  5165  copsexgwOLD  5456  nfiotadw  6475  iota2d  6504  iota2  6505  riota5f  7376  oprabidw  7422  opiota  8035  mpoxopoveq  8193  nfttrcld  9659  axrepndlem1  10544  axunndlem1  10547  fproddivf  16008  nfchnd  18634  xrofsup  32930  dvelimalcasei  35332  dvelimexcasei  35334  axsepg2  35397  axsepg3  35398  axsepg3ALT  35399  axsepg4  35400  axsepg5  35401  axnulg  35402  axpowg2  35404  axpowg3  35405  bj-cbvaldvav  37249  bj-cbvexdvav  37250  opelopabbv  37596  brabd  37601  cbveud  37827  cbvreud  37828  fvineqsneu  37866  wl-mo2t  38039  wl-sb8eut  38042  wl-sb8eutv  38043  wl-issetft  38046  riotasv2d  39542  cdleme42b  41063  dihvalcqpre  41820  mapdheq  42313  hdmap1eq  42386  hdmapval2lem  42416