Theorem nfvd 1919

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

Syntax hints:   → wi 4  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  cbvaldw  2337  cbvald  2407  cbvaldva  2409  cbvexdva  2410  sbiedv  2508  nfmodv  2559  nfabdw  2929  vtoclgft  3482  vtocldOLD  3485  sbciedOLD  3757  nfunid  4842  nfopabd  5138  copsexgw  5398  nfiotadw  6379  iota2d  6406  iota2  6407  riota5f  7241  oprabidw  7286  opiota  7872  mpoxopoveq  8006  axrepndlem1  10279  axunndlem1  10282  fproddivf  15625  xrofsup  30992  nfttrcld  33696  bj-cbvaldvav  34912  bj-cbvexdvav  34913  opelopabbv  35241  brabd  35246  cbveud  35470  cbvreud  35471  fvineqsneu  35509  wl-mo2t  35657  wl-sb8eut  35659  riotasv2d  36898  cdleme42b  38419  dihvalcqpre  39176  mapdheq  39669  hdmap1eq  39742  hdmapval2lem  39772