Theorem nfvd 1916

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

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvaldw  2347  cbvald  2417  cbvaldva  2419  cbvexdva  2420  sbiedv  2523  nfmodv  2618  vtoclgft  3501  vtocld  3504  sbcied  3762  nfunid  4806  copsexgw  5346  nfiotadw  6286  iota2d  6312  iota2  6313  riota5f  7121  oprabidw  7166  opiota  7739  mpoxopoveq  7868  axrepndlem1  10003  axunndlem1  10006  fproddivf  15333  xrofsup  30518  bj-cbvaldvav  34240  bj-cbvexdvav  34241  opelopabbv  34558  brabd  34563  cbveud  34789  cbvreud  34790  fvineqsneu  34828  wl-mo2t  34976  wl-sb8eut  34978  riotasv2d  36253  cdleme42b  37774  dihvalcqpre  38531  mapdheq  39024  hdmap1eq  39097  hdmapval2lem  39127