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

Theorem nfvd 1831
 Description: nfv 1830 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1812. (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 1830 . 2 𝑥𝜓
21a1i 11 1 (𝜑 → Ⅎ𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701 This theorem is referenced by:  cbvald  2265  cbvaldvaOLD  2270  cbvexdvaOLD  2272  sbiedv  2398  vtocld  3230  sbcied  3439  nfunid  4379  iota2d  5793  iota2  5794  riota5f  6535  opiota  7118  mpt2xopoveq  7232  axrepndlem1  9293  axunndlem1  9296  fproddivf  14557  xrofsup  28923  bj-cbvaldvav  31928  bj-cbvexdvav  31929  wl-mo2t  32536  wl-sb8eut  32538  riotasv2d  33261  cdleme42b  34784  dihvalcqpre  35542  mapdheq  36035  hdmap1eq  36109  hdmapval2lem  36141
 Copyright terms: Public domain W3C validator