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  2368  cbvald  2437  cbvaldva  2439  cbvexdva  2440  sbiedv  2534  nfmodv  2585  nfabdw  2944  cbvexeqsetf  3466  nfunid  4873  nfopabd  5173  copsexgwOLD  5461  nfiotadw  6496  iota2d  6525  iota2  6526  riota5f  7403  oprabidw  7449  opiota  8068  mpoxopoveq  8229  nfttrcld  9704  axrepndlem1  10670  axunndlem1  10673  fproddivf  16147  nfchnd  18778  xrofsup  33352  dvelimalcasei  35699  dvelimexcasei  35701  axsepg2  35791  axsepg3  35792  axsepg3ALT  35793  axsepg4  35794  axsepg5  35795  axnulg  35796  axpowg2  35798  axpowg3  35799  bj-cbvaldvav  37695  bj-cbvexdvav  37696  opelopabbv  38044  brabd  38049  cbveud  38275  cbvreud  38276  fvineqsneu  38314  wl-mo2t  38487  wl-sb8eut  38490  wl-sb8eutv  38491  wl-issetft  38494  findcard4  38612  riotasv2d  39994  cdleme42b  41515  dihvalcqpre  42272  mapdheq  42765  hdmap1eq  42838  hdmapval2lem  42868