Theorem nfvd 1918

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

Syntax hints:   → wi 4  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  cbvaldw  2335  cbvald  2407  cbvaldva  2409  cbvexdva  2410  sbiedv  2508  nfmodv  2559  nfabdw  2930  vtoclgft  3492  vtocldOLD  3495  sbciedOLD  3762  nfunid  4845  nfopabd  5142  copsexgw  5404  nfiotadw  6394  iota2d  6421  iota2  6422  riota5f  7261  oprabidw  7306  opiota  7899  mpoxopoveq  8035  nfttrcld  9468  axrepndlem1  10348  axunndlem1  10351  fproddivf  15697  xrofsup  31090  bj-cbvaldvav  34985  bj-cbvexdvav  34986  opelopabbv  35314  brabd  35319  cbveud  35543  cbvreud  35544  fvineqsneu  35582  wl-mo2t  35730  wl-sb8eut  35732  riotasv2d  36971  cdleme42b  38492  dihvalcqpre  39249  mapdheq  39742  hdmap1eq  39815  hdmapval2lem  39845