Theorem nfvd 1913

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

Syntax hints:   → wi 4  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781

This theorem is referenced by:  cbvaldw  2339  cbvald  2410  cbvaldva  2412  cbvexdva  2413  sbiedv  2507  nfmodv  2557  nfabdw  2925  cbvexeqsetf  3493  sbciedOLD  3838  nfunid  4918  nfopabd  5216  copsexgw  5501  nfiotadw  6519  iota2d  6551  iota2  6552  riota5f  7416  oprabidw  7462  opiota  8083  mpoxopoveq  8243  nfttrcld  9748  axrepndlem1  10630  axunndlem1  10633  fproddivf  16020  xrofsup  32778  dvelimalcasei  35069  dvelimexcasei  35071  axsepg2  35075  axsepg2ALT  35076  axnulg  35085  bj-cbvaldvav  36786  bj-cbvexdvav  36787  opelopabbv  37126  brabd  37131  cbveud  37355  cbvreud  37356  fvineqsneu  37394  wl-mo2t  37556  wl-sb8eut  37559  wl-sb8eutv  37560  wl-issetft  37563  riotasv2d  38939  cdleme42b  40461  dihvalcqpre  41218  mapdheq  41711  hdmap1eq  41784  hdmapval2lem  41814