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

Theorem nfrd 1743
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 1741 . 2  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
31, 2syl 15 1  |-  ( ph  ->  ( ps  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  alrimdd  1748  19.9t  1782  19.21t  1790  nfim1  1821  nfan1  1822  cbv1  1919  cbv2  1921  sbied  1976  sbal1  2065  abidnf  2934  eusvnfb  4530  axrepnd  8216  axacndlem4  8232
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator