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

Theorem nfvd 1729
Description: nfv 1728 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1945. (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nfvd  |-  ( ph  ->  F/ x ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem nfvd
StepHypRef Expression
1 nfv 1728 . 2  |-  F/ x ps
21a1i 11 1  |-  ( ph  ->  F/ x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-5 1725
This theorem depends on definitions:  df-bi 185  df-nf 1638
This theorem is referenced by:  cbvald  2052  cbvaldva  2058  cbvexdva  2059  sbiedv  2176  vtocld  3108  sbcied  3313  nfunid  4197  iota2d  5557  iota2  5558  riota5f  6263  opiota  6842  mpt2xopoveq  6949  axrepndlem1  8998  axunndlem1  9001  xrofsup  28016  bj-cbvaldvav  30857  bj-cbvexdvav  30858  wl-mo2t  31372  wl-sb8eut  31374  riotasv2d  31961  cdleme42b  33477  dihvalcqpre  34235  mapdheq  34728  hdmap1eq  34802  hdmapval2lem  34834  fproddivf  36937
  Copyright terms: Public domain W3C validator