Theorem nfvd 1919

Description: nfv 1918 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1898. (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 1918	. 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 1914

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  2504  nfmodv  2554  nfabdw  2927  vtoclgft  3541  vtocldOLD  3544  sbciedOLD  3824  nfunid  4915  nfopabd  5217  copsexgw  5491  nfiotadw  6499  iota2d  6532  iota2  6533  riota5f  7394  oprabidw  7440  opiota  8045  mpoxopoveq  8204  nfttrcld  9705  axrepndlem1  10587  axunndlem1  10590  fproddivf  15931  xrofsup  31980  bj-cbvaldvav  35681  bj-cbvexdvav  35682  opelopabbv  36024  brabd  36029  cbveud  36253  cbvreud  36254  fvineqsneu  36292  wl-mo2t  36440  wl-sb8eut  36442  wl-issetft  36444  riotasv2d  37827  cdleme42b  39349  dihvalcqpre  40106  mapdheq  40599  hdmap1eq  40672  hdmapval2lem  40702