Theorem nfvd 1844

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

Syntax hints:   → wi 4  Ⅎwnf 1708

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

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  cbvald  2277  cbvaldvaOLD  2282  cbvexdvaOLD  2284  sbiedv  2410  vtocld  3257  sbcied  3472  nfunid  4443  iota2d  5876  iota2  5877  riota5f  6636  opiota  7229  mpt2xopoveq  7345  axrepndlem1  9414  axunndlem1  9417  fproddivf  14718  xrofsup  29533  bj-cbvaldvav  32741  bj-cbvexdvav  32742  wl-mo2t  33357  wl-sb8eut  33359  riotasv2d  34243  cdleme42b  35766  dihvalcqpre  36524  mapdheq  37017  hdmap1eq  37091  hdmapval2lem  37123