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

Theorem nfvd 2011
Description: nfv 2010 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1993. (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 2010 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-ex 1876  df-nf 1880
This theorem is referenced by:  cbvald  2414  sbiedv  2527  nfmodv  2604  vtocld  3444  sbcied  3670  nfunid  4635  iota2d  6089  iota2  6090  riota5f  6864  opiota  7464  mpt2xopoveq  7583  axrepndlem1  9702  axunndlem1  9705  fproddivf  15054  xrofsup  30051  bj-cbvaldvav  33245  bj-cbvexdvav  33246  wl-mo2t  33847  wl-sb8eut  33849  riotasv2d  34978  cdleme42b  36499  dihvalcqpre  37256  mapdheq  37749  hdmap1eq  37822  hdmapval2lem  37852
  Copyright terms: Public domain W3C validator