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

Theorem nfrd 1429
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 1427 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 14 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nfan1  1472  nfim1  1479  alrimdd  1516  spimed  1644  cbv2  1651  nfald  1659  sbied  1687  cbvexd  1818  sbcomxyyz  1862  hbsbd  1874  dvelimALT  1902  dvelimfv  1903  hbeud  1938  abidnf  2732  eusvnfb  4214
  Copyright terms: Public domain W3C validator