Theorem nfvd 1831

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

Syntax hints:   → wi 4  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  cbvald  2265  cbvaldvaOLD  2270  cbvexdvaOLD  2272  sbiedv  2398  vtocld  3230  sbcied  3439  nfunid  4379  iota2d  5793  iota2  5794  riota5f  6535  opiota  7118  mpt2xopoveq  7232  axrepndlem1  9293  axunndlem1  9296  fproddivf  14557  xrofsup  28923  bj-cbvaldvav  31928  bj-cbvexdvav  31929  wl-mo2t  32536  wl-sb8eut  32538  riotasv2d  33261  cdleme42b  34784  dihvalcqpre  35542  mapdheq  36035  hdmap1eq  36109  hdmapval2lem  36141