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

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
StepHypRef Expression
1 nfv 1915 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
 Colors of variables: wff setvar class 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  2577  vtoclgft  3472  vtocldOLD  3476  sbcied  3741  nfunid  4807  copsexgw  5352  nfiotadw  6301  iota2d  6327  iota2  6328  riota5f  7141  oprabidw  7186  opiota  7766  mpoxopoveq  7900  axrepndlem1  10057  axunndlem1  10060  fproddivf  15394  xrofsup  30618  bj-cbvaldvav  34547  bj-cbvexdvav  34548  opelopabbv  34864  brabd  34869  cbveud  35095  cbvreud  35096  fvineqsneu  35134  wl-mo2t  35282  wl-sb8eut  35284  riotasv2d  36559  cdleme42b  38080  dihvalcqpre  38837  mapdheq  39330  hdmap1eq  39403  hdmapval2lem  39433
 Copyright terms: Public domain W3C validator