MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfvd Structured version   Visualization version   GIF version

Theorem nfvd 1909
Description: nfv 1908 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1888. (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nfvd (𝜑 → Ⅎ𝑥𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfvd
StepHypRef Expression
1 nfv 1908 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778
This theorem is referenced by:  cbvaldw  2352  cbvald  2424  cbvaldva  2426  cbvexdva  2427  sbiedv  2544  nfmodv  2640  ralcom2w  3367  vtoclgft  3558  vtocld  3561  sbcied  3817  nfunid  4842  copsexgw  5377  nfiotadw  6314  iota2d  6340  iota2  6341  riota5f  7137  oprabidw  7182  opiota  7751  mpoxopoveq  7879  axrepndlem1  10006  axunndlem1  10009  fproddivf  15333  xrofsup  30407  bj-cbvaldvav  34011  bj-cbvexdvav  34012  opelopabbv  34316  brabd  34321  cbveud  34524  cbvreud  34525  fvineqsneu  34563  wl-mo2t  34680  wl-sb8eut  34682  riotasv2d  35962  cdleme42b  37483  dihvalcqpre  38240  mapdheq  38733  hdmap1eq  38806  hdmapval2lem  38836
  Copyright terms: Public domain W3C validator