Theorem nfvd 1914

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

Syntax hints:   → wi 4  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  cbvaldw  2344  cbvald  2415  cbvaldva  2417  cbvexdva  2418  sbiedv  2512  nfmodv  2562  nfabdw  2932  cbvexeqsetf  3503  sbciedOLD  3851  nfunid  4937  nfopabd  5234  copsexgw  5510  nfiotadw  6528  iota2d  6561  iota2  6562  riota5f  7433  oprabidw  7479  opiota  8100  mpoxopoveq  8260  nfttrcld  9779  axrepndlem1  10661  axunndlem1  10664  fproddivf  16035  xrofsup  32774  dvelimalcasei  35052  dvelimexcasei  35054  axsepg2  35058  axsepg2ALT  35059  axnulg  35068  bj-cbvaldvav  36769  bj-cbvexdvav  36770  opelopabbv  37109  brabd  37114  cbveud  37338  cbvreud  37339  fvineqsneu  37377  wl-mo2t  37529  wl-sb8eut  37532  wl-sb8eutv  37533  wl-issetft  37536  riotasv2d  38913  cdleme42b  40435  dihvalcqpre  41192  mapdheq  41685  hdmap1eq  41758  hdmapval2lem  41788