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

Theorem nf5rd 2198
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 2195 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-ex 1787  df-nf 1791
This theorem is referenced by:  spimedv  2199  alrimdd  2216  nf5di  2289  hbnt  2298  hbimd  2302  dvelimhw  2348  dveeq2  2378  dveeq1  2380  axc9  2382  spimed  2388  dvelimh  2450  abidnf  3602  eusvnfb  5260  axrepnd  10094  axacndlem4  10110  bj-cbv2v  34623  bj-elgab  34770  wl-nfeqfb  35338
  Copyright terms: Public domain W3C validator