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

Theorem nfvd 1841
Description: nfv 1840 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1820. (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 1840 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  cbvald  2276  cbvaldvaOLD  2281  cbvexdvaOLD  2283  sbiedv  2409  vtocld  3246  sbcied  3458  nfunid  4414  iota2d  5840  iota2  5841  riota5f  6596  opiota  7181  mpt2xopoveq  7297  axrepndlem1  9366  axunndlem1  9369  fproddivf  14654  xrofsup  29400  bj-cbvaldvav  32418  bj-cbvexdvav  32419  wl-mo2t  33024  wl-sb8eut  33026  riotasv2d  33758  cdleme42b  35281  dihvalcqpre  36039  mapdheq  36532  hdmap1eq  36606  hdmapval2lem  36638
  Copyright terms: Public domain W3C validator