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

Theorem nfrd 1930
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 1928 . 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 1435   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  alrimdd  1935  nfdi  1976  nfim1  1979  hbimd  1981  nfan1  1987  nfald  2011  dvelimhw  2015  spimed  2065  cbv2  2078  dveeq2  2101  dveeq1  2103  axc9  2105  dvelimh  2137  abidnf  3239  eusvnfb  4620  axrepnd  9026  axacndlem4  9042  bj-spimedv  31280  bj-cbv2v  31295  wl-nfeqfb  31834
  Copyright terms: Public domain W3C validator