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 1785

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 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2347  cbvald  2417  cbvaldva  2419  cbvexdva  2420  sbiedv  2523  nfmodv  2577  vtoclgft  3472  vtocldOLD  3476  sbcied  3741  nfunid  4807  copsexgw  5352  nfiotadw  6301  iota2d  6327  iota2  6328  riota5f  7141  oprabidw  7186  opiota  7766  mpoxopoveq  7900  axrepndlem1  10057  axunndlem1  10060  fproddivf  15394  xrofsup  30618  bj-cbvaldvav  34547  bj-cbvexdvav  34548  opelopabbv  34864  brabd  34869  cbveud  35095  cbvreud  35096  fvineqsneu  35134  wl-mo2t  35282  wl-sb8eut  35284  riotasv2d  36559  cdleme42b  38080  dihvalcqpre  38837  mapdheq  39330  hdmap1eq  39403  hdmapval2lem  39433