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

Theorem nfrd 1764
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 1762 . 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 1540   F/wnf 1544
This theorem is referenced by:  alrimdd  1769  nfim1  1813  nfim1OLD  1814  hbimd  1817  nfan1  1828  nfald  1857  19.9tOLD  1862  19.21tOLD  1868  cbv1  1984  cbv2  1986  sbied  2041  sbal1  2131  abidnf  3010  eusvnfb  4612  axrepnd  8306  axacndlem4  8322  cbv1wAUX7  28935  cbv2wAUX7  28937  sbiedNEW7  28961  sbal1NEW7  29033  cbv1OLD7  29121  cbv2OLD7  29123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator