MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nf5rd Structured version   Visualization version   GIF version

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

Proof of Theorem nf5rd
StepHypRef Expression
1 nf5rd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nf5r 2193 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783
This theorem is referenced by:  spimedv  2196  alrimdd  2213  nf5di  2284  hbnt  2293  hbimd  2297  dvelimhw  2346  dveeq2  2382  dveeq1  2384  axc9  2386  spimed  2392  dvelimh  2454  abidnf  3707  eusvnfb  5392  axrepnd  10635  axacndlem4  10651  bj-cbv2v  36800  bj-elgab  36941  wl-nfeqfb  37538
  Copyright terms: Public domain W3C validator