ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfrd Unicode version

Theorem nfrd 1458
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 1456 . 2  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287   F/wnf 1394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nfan1  1501  nfim1  1508  alrimdd  1545  spimed  1675  cbv2  1682  nfald  1690  sbied  1718  cbvexd  1850  sbcomxyyz  1894  hbsbd  1906  dvelimALT  1934  dvelimfv  1935  hbeud  1970  abidnf  2781  eusvnfb  4267
  Copyright terms: Public domain W3C validator