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

Theorem nf5rd 2194
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 2192 . 2 (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
31, 2syl 17 1 (𝜑 → (𝜓 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781
This theorem is referenced by:  spimedv  2195  alrimdd  2212  nf5di  2284  hbnt  2293  hbimd  2297  dvelimhw  2346  dveeq2  2381  dveeq1  2383  axc9  2385  spimed  2391  dvelimh  2453  abidnf  3711  eusvnfb  5399  axrepnd  10632  axacndlem4  10648  bj-cbv2v  36781  bj-elgab  36922  wl-nfeqfb  37517
  Copyright terms: Public domain W3C validator