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

Theorem nfrd 1410
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfrd.1 (φ → Ⅎxψ)
Assertion
Ref Expression
nfrd (φ → (ψxψ))

Proof of Theorem nfrd
StepHypRef Expression
1 nfrd.1 . 2 (φ → Ⅎxψ)
2 nfr 1408 . 2 (Ⅎxψ → (ψxψ))
31, 2syl 14 1 (φ → (ψxψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nfan1  1453  nfim1  1460  alrimdd  1497  spimed  1625  cbv2  1632  nfald  1640  sbied  1668  cbvexd  1799  sbcomxyyz  1843  hbsbd  1855  dvelimALT  1883  dvelimfv  1884  hbeud  1919  abidnf  2703  eusvnfb  4152
  Copyright terms: Public domain W3C validator