Theorem nfvd 1910

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

Syntax hints:   → wi 4  Ⅎwnf 1777

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

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  cbvaldw  2328  cbvald  2400  cbvaldva  2402  cbvexdva  2403  sbiedv  2497  nfmodv  2547  nfabdw  2915  issetft  3475  vtocldOLD  3539  sbciedOLD  3820  nfunid  4915  nfopabd  5217  copsexgw  5492  nfiotadw  6504  iota2d  6537  iota2  6538  riota5f  7404  oprabidw  7450  opiota  8064  mpoxopoveq  8225  nfttrcld  9735  axrepndlem1  10617  axunndlem1  10620  fproddivf  15967  xrofsup  32619  bj-cbvaldvav  36411  bj-cbvexdvav  36412  opelopabbv  36753  brabd  36758  cbveud  36982  cbvreud  36983  fvineqsneu  37021  wl-mo2t  37173  wl-sb8eut  37176  wl-sb8eutv  37177  wl-issetft  37180  riotasv2d  38559  cdleme42b  40081  dihvalcqpre  40838  mapdheq  41331  hdmap1eq  41404  hdmapval2lem  41434