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

Theorem nfrd 1485
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfrd.1 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfrd (𝜑 → (𝜓 → ∀𝑥𝜓))

Proof of Theorem nfrd
StepHypRef Expression
1 nfrd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nfr 1483 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 14 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wnf 1421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nfan1  1528  nfim1  1535  alrimdd  1573  spimed  1703  cbv2  1710  nfald  1718  sbied  1746  cbvexd  1879  sbcomxyyz  1923  hbsbd  1935  dvelimALT  1963  dvelimfv  1964  hbeud  1999  abidnf  2825  eusvnfb  4345
  Copyright terms: Public domain W3C validator