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

Theorem nfrd 1775
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 1773 . 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 1546   F/wnf 1550
This theorem is referenced by:  alrimdd  1780  nfim1  1826  nfim1OLD  1827  hbimd  1830  nfan1  1841  nfald  1867  dvelimhw  1872  19.9tOLD  1876  19.21tOLD  1882  spimed  1958  ax12olem4  1975  dveeq1  1987  dvelimh  2015  cbv1  2032  cbv2  2034  sbied  2085  sbal1  2176  abidnf  3063  eusvnfb  4678  axrepnd  8425  axacndlem4  8441  cbv1wAUX7  29218  cbv2wAUX7  29220  sbiedNEW7  29244  sbal1NEW7  29316  cbv1OLD7  29404  cbv2OLD7  29406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator