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

Theorem nfrd 1779
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 1777 . 2  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
31, 2syl 16 1  |-  ( ph  ->  ( ps  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549   F/wnf 1553
This theorem is referenced by:  alrimdd  1784  nfim1  1830  nfim1OLD  1831  hbimd  1834  nfan1  1845  nfald  1871  dvelimhw  1876  19.9tOLD  1880  19.21tOLD  1886  spimed  1960  cbv1OLD  1976  cbv2  1980  cbv2OLD  1981  ax12o  2010  dveeq1  2021  dvelimh  2071  sbiedOLD  2151  sbal1  2203  abidnf  3103  eusvnfb  4719  axrepnd  8469  axacndlem4  8485  cbv1wAUX7  29512  cbv2wAUX7  29514  sbiedNEW7  29540  sb8dwAUX7  29590  sbal1NEW7  29615  cbv1OLD7  29720  cbv2OLD7  29722
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator