Theorem nfvd 1948

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  cbvaldw  2367  cbvald  2436  cbvaldva  2438  cbvexdva  2439  sbiedv  2533  nfmodv  2584  nfabdw  2943  cbvexeqsetf  3465  nfunid  4873  nfopabd  5173  copsexgwOLD  5467  nfiotadw  6492  iota2d  6521  iota2  6522  riota5f  7398  oprabidw  7444  opiota  8056  mpoxopoveq  8217  nfttrcld  9689  axrepndlem1  10601  axunndlem1  10604  fproddivf  16074  nfchnd  18699  xrofsup  33238  dvelimalcasei  35585  dvelimexcasei  35587  axsepg2  35666  axsepg3  35667  axsepg3ALT  35668  axsepg4  35669  axsepg5  35670  axnulg  35671  axpowg2  35673  axpowg3  35674  bj-cbvaldvav  37546  bj-cbvexdvav  37547  opelopabbv  37895  brabd  37900  cbveud  38126  cbvreud  38127  fvineqsneu  38165  wl-mo2t  38338  wl-sb8eut  38341  wl-sb8eutv  38342  wl-issetft  38345  findcard4  38463  riotasv2d  39830  cdleme42b  41351  dihvalcqpre  42108  mapdheq  42601  hdmap1eq  42674  hdmapval2lem  42704