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

Theorem nfrd 1390
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 1388 . 2 (Ⅎxψ → (ψxψ))
31, 2syl 14 1 (φ → (ψxψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224  wnf 1325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1377
This theorem depends on definitions:  df-bi 110  df-nf 1326
This theorem is referenced by:  nfan1  1434  nfim1  1441  alrimdd  1478  spimed  1606  cbv2  1613  nfald  1621  sbied  1649  cbvexd  1780  sbcomxyyz  1824  hbsbd  1836  dvelimALT  1864  dvelimfv  1865  hbeud  1900  abidnf  2682  eusvnfb  4132
  Copyright terms: Public domain W3C validator