Theorem nfvd 1915

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 209  df-ex 1780  df-nf 1784

This theorem is referenced by:  cbvaldw  2357  cbvald  2427  cbvaldva  2429  cbvexdva  2430  sbiedv  2545  nfmodv  2642  vtoclgft  3556  vtocld  3559  sbcied  3817  nfunid  4847  copsexgw  5384  nfiotadw  6320  iota2d  6346  iota2  6347  riota5f  7145  oprabidw  7190  opiota  7760  mpoxopoveq  7888  axrepndlem1  10017  axunndlem1  10020  fproddivf  15344  xrofsup  30495  bj-cbvaldvav  34129  bj-cbvexdvav  34130  opelopabbv  34439  brabd  34444  cbveud  34657  cbvreud  34658  fvineqsneu  34696  wl-mo2t  34815  wl-sb8eut  34817  riotasv2d  36097  cdleme42b  37618  dihvalcqpre  38375  mapdheq  38868  hdmap1eq  38941  hdmapval2lem  38971