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 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  cbvaldw  2358  cbvald  2428  cbvaldva  2430  cbvexdva  2431  sbiedv  2546  nfmodv  2643  vtoclgft  3555  vtocld  3558  sbcied  3816  nfunid  4846  copsexgw  5383  nfiotadw  6319  iota2d  6345  iota2  6346  riota5f  7144  oprabidw  7189  opiota  7759  mpoxopoveq  7887  axrepndlem1  10016  axunndlem1  10019  fproddivf  15343  xrofsup  30494  bj-cbvaldvav  34127  bj-cbvexdvav  34128  opelopabbv  34437  brabd  34442  cbveud  34655  cbvreud  34656  fvineqsneu  34694  wl-mo2t  34813  wl-sb8eut  34815  riotasv2d  36095  cdleme42b  37616  dihvalcqpre  38373  mapdheq  38866  hdmap1eq  38939  hdmapval2lem  38969