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

Theorem nfrd 1964
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfrd.1  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfrd  |-  ( ph  ->  ( ps  ->  A. x ps ) )

Proof of Theorem nfrd
StepHypRef Expression
1 nfrd.1 . 2  |-  ( ph  ->  F/ x ps )
2 nfr 1962 . 2  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
31, 2syl 17 1  |-  ( ph  ->  ( ps  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1453   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  alrimdd  1969  nfdi  2010  nfim1  2013  hbimd  2015  nfan1  2021  nfald  2045  dvelimhw  2071  spimed  2110  cbv2  2124  dveeq2  2147  dveeq1  2149  axc9  2151  dvelimh  2181  abidnf  3219  eusvnfb  4616  axrepnd  9050  axacndlem4  9066  bj-spimedv  31366  bj-cbv2v  31379  wl-nfeqfb  31916
  Copyright terms: Public domain W3C validator